[GHC] #12176: Failure of bidirectional type inference at the kind level
GHC
ghc-devs at haskell.org
Mon Jul 31 15:57:37 UTC 2017
#12176: Failure of bidirectional type inference at the kind level
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner: goldfire
Type: bug | Status: closed
Priority: normal | Milestone: 8.4.1
Component: Compiler | Version: 8.0.1
Resolution: fixed | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
| dependent/should_compile/T12176
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Changes (by bgamari):
* status: merge => closed
* resolution: => fixed
* milestone: => 8.4.1
Old description:
> I'm feeling particularly sadistic towards GHC at the moment, and so I fed
> it this:
>
> {{{
> import Data.Kind
>
> data Proxy :: forall k. k -> Type where
> MkProxy :: forall k (a :: k). Proxy a
>
> data X where
> MkX :: forall (k :: Type) (a :: k). Proxy a -> X
>
> type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
>
> type family Foo (x :: forall (a :: k). Proxy a -> X) where
> Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
> }}}
>
> Incredibly, GHC accepts it! And it even means what I wish it to, with
> GHCi telling me the following (with `-fprint-explicit-kinds`):
>
> {{{
> λ> :i Foo
> type family Foo k (x :: forall (a :: k). Proxy k a -> X)
> :: Proxy * k
> where [k] Foo k ('MkX k) = 'MkProxy * k
> }}}
>
> That is, I wished to extract the kind parameter to `MkK`, matching
> against a partially-applied `MkX`, and GHC understood that intention.
>
> However, sadly, writing `Foo Expr` produces
>
> {{{
> • Expected kind ‘forall (a :: k0). Proxy k0 a -> X’,
> but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’
> • In the first argument of ‘Foo’, namely ‘Expr’
> In the type ‘Foo Expr’
> In the type family declaration for ‘XXX’
> }}}
>
> For some reason, `Expr` is getting instantiated when it shouldn't be.
>
> Perhaps there's a simpler test case demonstrating the bug, but I feel so
> gleeful that this chicanery is accepted at all that I wanted to post.
New description:
I'm feeling particularly sadistic towards GHC at the moment, and so I fed
it this:
{{{#!hs
import Data.Kind
data Proxy :: forall k. k -> Type where
MkProxy :: forall k (a :: k). Proxy a
data X where
MkX :: forall (k :: Type) (a :: k). Proxy a -> X
type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
type family Foo (x :: forall (a :: k). Proxy a -> X) where
Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
}}}
Incredibly, GHC accepts it! And it even means what I wish it to, with GHCi
telling me the following (with `-fprint-explicit-kinds`):
{{{
λ> :i Foo
type family Foo k (x :: forall (a :: k). Proxy k a -> X)
:: Proxy * k
where [k] Foo k ('MkX k) = 'MkProxy * k
}}}
That is, I wished to extract the kind parameter to `MkK`, matching against
a partially-applied `MkX`, and GHC understood that intention.
However, sadly, writing `Foo Expr` produces
{{{
• Expected kind ‘forall (a :: k0). Proxy k0 a -> X’,
but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’
• In the first argument of ‘Foo’, namely ‘Expr’
In the type ‘Foo Expr’
In the type family declaration for ‘XXX’
}}}
For some reason, `Expr` is getting instantiated when it shouldn't be.
Perhaps there's a simpler test case demonstrating the bug, but I feel so
gleeful that this chicanery is accepted at all that I wanted to post.
--
Comment:
Given that this isn't a regression of 8.2 I'm going to punt this off until
8.4.1 unless someone objects.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12176#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list