GitLab

With a small boatload of GHC extensions, I can write a view pattern with Data.Typeable that will simulate something like case analysis on types:

{-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables,
             TypeApplications, TypeOperators, ViewPatterns #-}

import Data.Typeable

viewEqT :: forall b a. (Typeable a, Typeable b) => a -> Maybe ((a :~: b), b)
viewEqT x = case eqT @a @b of
  Just Refl -> Just (Refl, x)
  Nothing -> Nothing

evilId :: Typeable a => a -> a
evilId (viewEqT @Int -> Just (Refl, n)) = n + 1
evilId (viewEqT @String -> Just (Refl, str)) = reverse str
evilId x = x

However, this is ugly. I would like to clean things up with a nice pattern synonym:

pattern EqT :: forall b a. (Typeable a, Typeable b) => (a ~ b) => b -> a
pattern EqT x <- (viewEqT @b -> Just (Refl, x))

Sadly, while this pattern typechecks, using it seems to be impossible. This program is rejected:

evilId :: Typeable a => a -> a
evilId (EqT (n :: Int)) = n + 1
evilId (EqT (str :: String)) = reverse str
evilId x = x

Specifically, it produces the following type error:

/private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:17:9: error:
    • Could not deduce (Typeable b0) arising from a pattern
      from the context: Typeable a
        bound by the type signature for:
                   evilId :: Typeable a => a -> a
        at library/TypeEqTest.hs:16:1-30
      The type variable ‘b0’ is ambiguous
    • In the pattern: EqT (n :: Int)
      In an equation for ‘evilId’: evilId (EqT (n :: Int)) = n + 1

/private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:17:14: error:
    • Could not deduce: a ~ Int
      from the context: a ~ b0
        bound by a pattern with pattern synonym:
                   EqT :: forall b a. (Typeable a, Typeable b) => a ~ b => b -> a,
                 in an equation for ‘evilId’
        at library/TypeEqTest.hs:17:9-22
      ‘a’ is a rigid type variable bound by
        the type signature for:
          evilId :: forall a. Typeable a => a -> a
        at library/TypeEqTest.hs:16:11
      Expected type: Int
        Actual type: b0
    • When checking that the pattern signature: Int
        fits the type of its context: b0
      In the pattern: n :: Int
      In the pattern: EqT (n :: Int)
    • Relevant bindings include
        evilId :: a -> a (bound at library/TypeEqTest.hs:17:1)

/private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:18:9: error:
    • Could not deduce (Typeable b1) arising from a pattern
      from the context: Typeable a
        bound by the type signature for:
                   evilId :: Typeable a => a -> a
        at library/TypeEqTest.hs:16:1-30
      The type variable ‘b1’ is ambiguous
    • In the pattern: EqT (str :: String)
      In an equation for ‘evilId’:
          evilId (EqT (str :: String)) = reverse str

/private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:18:14: error:
    • Could not deduce: a ~ String
      from the context: a ~ b1
        bound by a pattern with pattern synonym:
                   EqT :: forall b a. (Typeable a, Typeable b) => a ~ b => b -> a,
                 in an equation for ‘evilId’
        at library/TypeEqTest.hs:18:9-27
      ‘a’ is a rigid type variable bound by
        the type signature for:
          evilId :: forall a. Typeable a => a -> a
        at library/TypeEqTest.hs:16:11
      Expected type: String
        Actual type: b1
    • When checking that the pattern signature: String
        fits the type of its context: b1
      In the pattern: str :: String
      In the pattern: EqT (str :: String)
    • Relevant bindings include
        evilId :: a -> a (bound at library/TypeEqTest.hs:17:1)

I would expect the program to typecheck, since in any other context, GHC would not have any trouble inferring the type of b for each use of EqT. However, it seems that pattern synonyms do not allow me to provide any type information “in”, only get type information “out”. Is there some fundamental limitation that forces this to be the case, or is this just a missing feature?

Trac metadata

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