Regression: Combination of GADTs and Type families
The function "fails" compiles in 6.12.3 but not in 7.1 HEAD.
{-# LANGUAGE TypeFamilies, EmptyDataDecls, GADTs #-}
type family F f :: *
data Id c = Id
type instance F (Id c) = c
data C :: * -> * where
C :: f -> C (W (F f))
data W :: * -> *
fails :: C a -> C a
fails (C _) = C Id
works :: C (W a) -> C (W a)
works (C _) = C Id
The error is:
Could not deduce (F (Id c) ~ F f) from the context (a ~ W (F f))
NB: `F' is a type function, and may not be injective
Expected type: a
Actual type: W (F (Id c))
In the expression: C Id
In an equation for `fails': fails (C _) = C Id
But in the function "works" the compiler apparently has no problem deducing (F (Id c) ~ F f).
Trac metadata
Trac field | Value |
---|---|
Version | 7.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |