Opened 3 years ago

Closed 3 years ago

#8985 closed bug (fixed)

Strange kind error with type family, GADTs, data kinds, and kind polymorphism

Reported by: kosmikus Owned by:
Priority: normal Milestone: 7.8.3
Component: Compiler (Type checker) Version: 7.8.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: polykinds/T8985
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


Consider the following test case (I've tried hard to make it minimal, which unfortunately means there's not a lot of intuition left):

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators #-}

data X (xs :: [k]) = MkX
data Y :: (k -> *) -> [k] -> * where
  MkY :: f x -> Y f (x ': xs)

type family F (a :: [[*]]) :: *
type instance F xss = Y X xss

works :: Y X '[ '[ ] ] -> ()
works (MkY MkX) = ()

fails :: F '[ '[ ] ] -> ()
fails (MkY MkX) = ()

This code compiles in GHC 7.6.3, but it fails in GHC 7.8.1 (both rc2 and the actual release) with the following error:

    Couldn't match kind ‘k0’ with ‘*’
    Expected type: F '['[]]
      Actual type: Y t0 t1
    In the pattern: MkY MkX
    In an equation for ‘fails’: fails (MkY MkX) = ()

    Couldn't match type ‘t0’ with ‘X’
      ‘t0’ is untouchable
        inside the constraints (t1 ~ (x : xs))
        bound by a pattern with constructor
                   MkY :: forall (f :: k -> *) (x :: k) (xs :: [k]).
                          f x -> Y f (x : xs),
                 in an equation for ‘fails’
        at TestCase.hs:14:8-14
    Expected type: t0 x
      Actual type: X x
    In the pattern: MkX
    In the pattern: MkY MkX
    In an equation for ‘fails’: fails (MkY MkX) = ()

I'm puzzled that simply adding the type family invokation makes the type checker fail with a kind error, even though the type family itself itsn't kind-polymorphic.

Change History (6)

comment:1 Changed 3 years ago by simonpj

Thank you. It's a palpable bug in the kind unifier. Working on it.

comment:2 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In e7f0ae7ff4f2199abe42f20bac825a7802bff466/ghc:

Honour the untouchability of kind variables

Trac #8985 showed up a major shortcoming in the kind unifier: it was
ignoring untoucability.  This has unpredictably-bad consequences;
notably, the skolem-escape check can fail.

There were two things wrong
 * TcRnMonad.isTouchableTcM was returning a constant value for kind variables
   (wrong), and even worse the constant was back-to-front (it was always False).

 * We weren't even calling isTouchableTcM in TcType.unifyKindX.

I'm not sure how this ever worked.

Merge to 7.8.3 in due course.

comment:3 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

comment:4 Changed 3 years ago by simonpj

Status: newmerge
Test Case: polykinds/T8985

Great catch, thank you.

Merge to 7.8.3.


comment:5 Changed 3 years ago by thoughtpolice

Milestone: 7.8.3

comment:6 Changed 3 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged to 7.8.

Note: See TracTickets for help on using tickets.