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

31 Jul 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