[GHC] #12176: Failure of bidirectional type inference at the kind level

[GHC]

#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