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