Opened 5 years ago

Closed 5 years ago

## #9954 closed bug (invalid)

# Required constraints are not inferred for pattern synonyms involving GADTs

Reported by: | cactus | Owned by: | cactus |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler (Type checker) | Version: | |

Keywords: | PatternSynonyms | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | GHC rejects valid program | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | #9953 | Differential Rev(s): | |

Wiki Page: |

### Description

Let's say we have the following setup:

{-# LANGUAGE GADTs, PatternSynonyms, ViewPatterns #-} data T a where MkT1 :: a -> T a MkT2 :: a -> T (Maybe a) f :: (Eq a) => a -> a f = id

Then the following definition works as expected:

pattern P1 x <- MkT1 (f -> x)

with the following inferred type:

λ» :i P1 pattern P1 :: () => Eq t => t -> T t

However, trying to do the same with {{MkT2}} doesn't work:

pattern P2 x <- MkT2 (f -> x)

this results in

Could not deduce (Eq a1) arising from a use of ‘f’ from the context (t ~ Maybe a1) bound by a pattern with constructor MkT2 :: forall a. a -> T (Maybe a), in a pattern synonym declaration

### Change History (2)

### comment:1 Changed 5 years ago by

### comment:2 Changed 5 years ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

**Note:**See TracTickets for help on using tickets.

This looks absolutely correct to me. Try it with an ordinary function, without the synonym:

and you get

And indeed, from where can we conjure up equality on the existentially-bound type?

So to me this looks like precisely the correct behaviour.

Siimon