#14104: Pattern synonyms work where constructors fail -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: This is behaving as expected. The types of the constructor `SZero` and the pattern synonym `S0` are almost the same, but not quite. You'll notice that if you leave off the type signature for `S0`, then `fromTrit` will fail to compile: {{{ Bug.hs:58:11: error: • Ambiguous type variable ‘n0’ arising from a pattern prevents the constraint ‘(KnownNatural n0)’ from being solved. Probable fix: use a type annotation to specify what ‘n0’ should be. These potential instances exist: instance KnownNatural n => KnownNatural ('Succ n) -- Defined at Bug.hs:42:10 instance KnownNatural 'Zero -- Defined at Bug.hs:40:10 • In the pattern: At S0 () In an equation for ‘fromTrit’: fromTrit (At S0 ()) = 0 | 58 | fromTrit (At S0 ()) = 0 | ^^^^^^^^ }}} Which is the same error you'd get if you tried using `SZero` in place of `S0` in the definition of `fromTrit`. The reason is that while the (written) type signature of `S0` is `SNatural 'Zero`, if you let GHC infer what it should be, then you'll get: {{{ λ> :i S0 pattern S0 :: () => n ~ 'Zero => SNatural n -- Defined at Bug.hs:47:1 }}} That is, `S0`'s inferred type is `SNatural n`, under the //given constraint// that `n` is equal to `Zero`. That is to say, in the context of a pattern match, we can only assume this equality //after// we've matched on it. This is why `fromTrit` is failing to typecheck with the constructor `SZero` (or `S0` with an inferred type), since we need evidence that `n ~ Zero` when matching on `At` (which comes before `SZero`/`S0`). To work around this issue, one can simply use the original pattern synonym type signatures, or one can try the workarounds that Syrak lists in this [https://www.reddit.com/r/haskell/comments/6so95h/why_do_pattern_synonyms_wor... helpful comment]. Really, all of this is a symptom of the way typechecking GADT patterns works. Intuitively, one might expect that GHC gathers all of the given constraints in every pattern of a clause before typechecking each pattern, but that's not how it works. In practice, GHC typechecks patterns in a [https://ghc.haskell.org/trac/ghc/ticket/12018 left-to-right, inside-out fashion]. This is compositional and works predictably, but is has the downside that there some sequences of patterns that will only typecheck if ordered in a certain way (and alas, `At SZero` is not ordered the right way). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14104#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler