Suggested type signature for a pattern synonym causes program to fail to type check

Take the following program:

{-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}

import Data.Typeable

data T where
  MkT :: Typeable a => a -> T

pattern Cast a <- MkT (cast -> Just a)

When compiled with -Wall, GHC rightly prompts about a missing signature on Cast:

    Top-level binding with no type signature:
      Cast :: forall b. Typeable b => forall a. Typeable a => b -> T

However, using this suggested type signature causes the program to fail to type check:

    • Could not deduce (Typeable a0)
        arising from the "provided" constraints claimed by
          the signature of ‘Cast’
      from the context: Typeable a
        bound by a pattern with constructor:
                   MkT :: forall a. Typeable a => a -> T,
                 in a pattern synonym declaration
        at ../foo.hs:9:19-38
      In other words, a successful match on the pattern
        MkT (cast -> Just a)
      does not provide the constraint (Typeable a0)
      The type variable ‘a0’ is ambiguous
    • In the declaration for pattern synonym ‘Cast’

Trac metadata

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