How can I write this template synonym without ambiguous type errors?

Question

Using ViewPatterns and Data.Typeable , I managed to write a function that allows me to write something similar to analyzing cases on types. Note:

 {-# LANGUAGE GADTs, PatternSynonyms, RankNTypes, 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 

The above evilId function evilId very evil, indeed, since it uses Typeable to completely suppress parametricity:

 ghci> evilId True True ghci> evilId "hello" "olleh" 

Since I like to be evil, I am very pleased with this, but the syntax above is very noisy. I would like to be able to write the same code more clearly, so I decided to write a synonym for the template:

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

I thought that I could use this template synonym to make analysis of my evil case a lot easier to read:

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

Unfortunately, this does not work at all. GHC does not seem to specify my type annotations before you check the template, so it considers b be an ambiguous variable in each template. Is there a way that I can cleanly wrap these templates with a synonym for the template, or will I stick with my longer viewing templates?

Answer 1

If the goal is to find a clean syntax to implement your evilId function, you can write it like this:

 {-# Language ScopedTypeVariables, GADTs, TypeApplications #-} module Demo where import Data.Typeable evilId :: forall a. Typeable a => a -> a evilId x | Just Refl <- eqT @a @Int = x+1 | Just Refl <- eqT @a @String = reverse x | otherwise = x 

This, unfortunately, does not help with the ambiguities surrounding your template synonyms.