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

### comment:4 Changed 3 years ago by

Status: | new → merge |
---|---|

Test Case: | → polykinds/T8985 |

Great catch, thank you.

Merge to 7.8.3.

Simon

### comment:5 Changed 3 years ago by

Milestone: | → 7.8.3 |
---|

**Note:**See TracTickets for help on using tickets.

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