#4484: Regression: Combination of GADTs and Type families
---------------------------------+------------------------------------------
Reporter: sjoerd_visscher | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler
Version: 7.1 | Keywords:
Testcase: | Blockedby:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: GHC rejects valid program
---------------------------------+------------------------------------------
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).
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4484>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
