#12176: Failure of bidirectional type inference at the kind level -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"1696dbf4ad0fda4d7c5b4afe1911cab51d7dd0b0/ghc" 1696dbf/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="1696dbf4ad0fda4d7c5b4afe1911cab51d7dd0b0" Fix #12176 by being a bit more careful instantiating. Previously, looking up a TyCon that said "no" to mightBeUnsaturated would then instantiate all of its invisible binders. But this is wrong for vanilla type synonyms, whose RHS kind might legitimately start with invisible binders. So a little more care is taken now, only to instantiate those invisible binders that need to be (so that the TyCon isn't unsaturated). }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12176#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#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

#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: | -------------------------------------+------------------------------------- Comment (by alpmestan): Nevermind, it seems like I somehow ended up not building with the patch from 4 days ago. This test passes from a fresh build with the tip of `master` from today. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12176#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler