#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: carlostome Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3981 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK I can see what is happening here. The trouble is with the COMPLETE pragma (again!). Suppose we'd written {{{ f :: Foo a -> a f (Foo1 x) = x f (MyFoo2 y) = y }}} This definition is rejected as ill-typed: {{{ T14135.hs:13:4: error: * Couldn't match type `a' with `Int' `a' is a rigid type variable bound by the type signature for: f :: forall a. Foo a -> a at T14135.hs:11:1-15 Expected type: Foo a Actual type: Foo Int }}} Reason: the pattern synonym `MyFoo2` demands that its scrutinee has type `Foo Int`. This is unlike a GADT, whose data constructors can have a return type `Foo Int` but which can match a scrutinee of type `Foo a`. It's a conscious design choice, described in the user manual (I hope). See `Note [Pattern synonym result type]` in `PatSyn`. Now, the overlap checker, when looking for missing patterns, effectively adds that extra equation. But the extra equation is ill-typed which crashes the overlap checker. (So yes, I think the `tcMatchTy` is fine; it's relying on the scrutinee having the right type.) So what are we to make of `{-# COMPLETE Foo1, MyFoo2 #-}`? The simplest thing to do is to insist that all the constructors in a COMPLETE pragma match the same type of scrutinee, where * A constructor `K` declared thus {{{ data T a b where K :: .... }}} matches a scrutinee of type `T a b` (NB: NOT the return type in K's signature which for a GADT might be `T Int Bool`) * A constructor `K` declared in a `data instance` {{{ data instance T ty1 ty2 where K :: .... }}} matches a scrutinee of type `T ty1 ty2`. (NB: again, not the return type in K's signature which may an instance of `K ty1 ty2`) * A constructor `K` declared in a pattern synonym {{{ pattern K :: .... -> T ty1 ty2 }}} matches a scrutinee of type `T ty1 ty2`. If we did this check when dealing with the COMPLETE pragma, I think that's solve this crash. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler