Ambiguous types with constraints on new variables

The following code fails to compile:

{-# LANGUAGE FlexibleContexts, TypeFamilies #-}

import Data.Typeable

type family Foo a

data C a

foo :: (Typeable (C z), z ~ Foo zp) => C zp
foo = undefined

with the error

    • Could not deduce (Typeable z)
      from the context: (Typeable (C z), z ~ Foo zp)
        bound by the type signature for:
                   foo :: (Typeable (C z), z ~ Foo zp) => C zp
        at Bug.hs:(9,8)-(10,9)
    • In the ambiguity check for ‘foo’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        foo :: (Typeable (C z), z ~ Foo zp) => C zp

It's quite unclear why GHC feels thta it needs Typeable z. The code compiles if I change the Typeable constraint to Typeable (C (Foo zp)), which should be identical to what I wrote.

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture