## Pattern synonyms should use type annotation information when typechecking

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 |