#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) 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): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: simonpj (added) Comment: Commit 6b77914cd37b697354611bcd87897885c1e5b4a6 (`Fix instantiation of pattern synonyms`) is responsible for this regression. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Wiki Page: | -------------------------------------+------------------------------------- Comment (by carlostome): I've found that this error is caused by the order of the arguments to `tcMatchTy` in the following code. {{{ mkOneConFull x con = do let res_ty = idType x (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty) = conLikeFullSig con tc_args = tyConAppArgs res_ty subst1 = case con of RealDataCon {} -> zipTvSubst univ_tvs tc_args PatSynCon {} -> expectJust "mkOneConFull" (tcMatchTy con_res_ty res_ty) ... }}} Adding some debugging information I noticed that the call that makes `tcMatchTy` return `Nothing` and therefore trigger the error it is done with the following arguments (as outputed with -dppr-debug): {{{ con_res_ty = main:T14135.Foo{tc r9} ghc-prim:GHC.Types.Int{(w) tc 3u} res_ty = main:T14135.Foo{tc r9} (a{tv aWz} [tv] :: *) }}} As far as I understand the problem stands because `tcMatchTy` expects the first argument to be a kind of template type that will get instantiated to match the second argument. However, it is clear that there is no substitution s such that s(Int) = a. If we change the call to `tcMatchTy res_ty con_res_ty` then the example program compiles fine but when trying to validate, ghc is not able to build anymore `Data.Typeable.Internal` because it triggers the exactly same error. I have found that by substituting `tcMatchTy` by `tcUnifyTy` we solve the full problem, however, I don't know if `tcMatchTy` should be prefered over `tcUnify` or not (if it makes a semantic difference). Any insight on this? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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, well, another alternative (triggered by #14253 comment:9), filter the candidate COMPLETE sets, to choose only those all of whose constructors match the type of the scrutinee. So in the example in comment:7 we'd use the COMPLETE pragma, but in the example in the Description we would ignore it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Anyone want to try doing this? Currently we just crash which is bad. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) 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: | -------------------------------------+------------------------------------- Changes (by carlostome): * owner: carlostome => (none) * status: patch => new Comment: I'm still stuck on this, and right now I don't have that much time to work on it. I'll drop it for someone else to work on it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: dfeuer 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 dfeuer): That is, try to learn something about what goes wrong in Phab:D3981. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: dfeuer 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 dfeuer): Something really weird is going on. I tried building GHC with profiling to trace down the problem, but that made it go away. If GHC is encountering a correctness problems ''compiling itself'', then we have serious trouble on our hands. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: dfeuer 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 duog): Hope this isn't all obvious: Of the four flavours [quick, prof, devel2-stage1, devel2-stage2], only devel2-stage2 is compiled with -DDEBUG and hence has the failing assertion enabled. I would expect that commenting out the assertion would have devl2-stage2 succeed as well (or fail on another assertion!). Either the assertion is wrong, or it's problem is later corrected (since core lint passes). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: dfeuer 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 dfeuer): I missed something that seems very important: the test failure Carlos describes does ''not'' occur with non-slow `./validate`, presumably because that doesn't enable debugging for the stage2 compiler. Indeed, I believe the problem with T13822 occurs ''without'' Carlos's patch! I'll verify tonight. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: dfeuer Type: bug | Status: closed Priority: highest | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: fixed | 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: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14135#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler