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: |
Description
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:
TestCase.hs:14:8: 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) = () TestCase.hs:14:12: 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
comment:2 Changed 3 years ago by Simon Peyton Jones <simonpj@…>
comment:3 Changed 3 years ago by Simon Peyton Jones <simonpj@…>
comment:4 Changed 3 years ago by simonpj
- Status changed from new to merge
- Test Case set to polykinds/T8985
Great catch, thank you.
Merge to 7.8.3.
Simon
comment:5 Changed 3 years ago by thoughtpolice
- Milestone set to 7.8.3
comment:6 Changed 3 years ago by thoughtpolice
- Resolution set to fixed
- Status changed from merge to closed
Merged to 7.8.
Note: See
TracTickets for help on using
tickets.
Thank you. It's a palpable bug in the kind unifier. Working on it.