Opened 14 months ago

Last modified 11 months ago

#12176 new bug

Failure of bidirectional type inference at the kind level

Reported by: goldfire Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

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.

Change History (0)

Note: See TracTickets for help on using tickets.