Opened 3 years ago

Closed 2 years ago

Last modified 20 months ago

#12176 closed bug (fixed)

Failure of bidirectional type inference at the kind level

Reported by: goldfire Owned by: goldfire
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc: alpmestan
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:

Description (last modified by bgamari)

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 (5)

comment:1 Changed 2 years ago by Richard Eisenberg <rae@…>

In 1696dbf/ghc:

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).

comment:2 Changed 2 years ago by goldfire

Status: newmerge
Test Case: dependent/should_compile/T12176

Merge if convenient, but I don't think this one ruins anyone's day.

comment:3 Changed 2 years ago by bgamari

Description: modified (diff)
Milestone: 8.4.1
Resolution: fixed
Status: mergeclosed

Given that this isn't a regression of 8.2 I'm going to punt this off until 8.4.1 unless someone objects.

comment:4 Changed 20 months ago by alpmestan

Cc: alpmestan added

I recently ran ./validate --slow and saw the test for this ticket (T12176) fail in all 5 ways that it supports. Just like with the test for #12442, it fails with:

ghc: panic! (the 'impossible' happened)
  (GHC version 8.5.20180329 for x86_64-unknown-linux):
        ASSERT failed! file compiler/typecheck/TcTyClsDecls.hs, line 1531

comment:5 Changed 20 months ago 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.

Note: See TracTickets for help on using tickets.