[GHC] #11524: Something is amiss with quantification in pattern synonym type signatures
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this program, {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TypeInType #-} module Test where data AType (a :: k) where AMaybe :: AType Maybe AInt :: AType Int AApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). AType a -> AType b -> AType (a b) pattern PApp :: () => (fun ~ a b) => AType a -> AType b -> AType fun --pattern PApp :: forall k (fun :: k) k1 (a :: k1 -> k) (b :: k1). -- () => (fun ~ a b) => AType a -> AType b -> AType fun pattern PApp fun arg <- AApp fun arg }}} I would have thought that the two type signatures would be equivalent. However, when I use the quantified signature GHC complains with, {{{ hi.hs:14:34: error: • Expected kind ‘AType a’, but ‘fun’ has kind ‘AType a1’ • In the declaration for pattern synonym ‘PApp’ • Relevant bindings include arg :: AType b1 (bound at hi.hs:14:34) fun :: AType a1 (bound at hi.hs:14:30) }}} Moreover, if I use the un-quantified signature and ask GHCi for the full type signature, it gives me the precisely the quantified type that it rejected previously, {{{ λ> :info PApp pattern PApp :: forall k (fun :: k) k1 (a :: k1 -> k) (b :: k1). () => fun ~ a b => AType a -> AType b -> AType fun -- Defined at hi.hs:14:1 }}} Very odd. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): If I understand pattern signatures correctly, it's a bug in the pretty- printer. Here is the correct version with explicit quantification: {{{ pattern PApp :: forall k2 (fun :: k2). () => forall k1 (a :: k1 -> k2) (b :: k1). (fun ~ a b) => AType a -> AType b -> AType fun }}} Note that `k2` and `fun` are universal, while `k1`, `a`, and `b` are existential. And indeed this signature is accepted. Two problems remain: 1. That error message is unhelpful. I imagine we can do better. 2. The pretty-printer should put the existentials in the right spot. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * cc: niteria (added) Comment:
It's a bug in the pretty-printer.
Actually, I'm not entirely sure that this is the whole story. After pulling I'm now seeing, {{{ $ inplace/bin/ghc-stage1 hi.hs [1 of 1] Compiling Main ( hi.hs, hi.o ) ghc-stage1: panic! (the 'impossible' happened) (GHC version 8.1.20160124 for x86_64-unknown-linux): ASSERT failed! file compiler/types/TyCoRep.hs line 1919 in_scope InScope {k_aB4 k_aJd a_aJe b_aJf} tenv [auE :-> a_aJe[tau:5], auF :-> b_aJf[tau:5], aB3 :-> k_aJd[tau:5]] cenv [] tys [fun_auD[sk] ~ a_auE[sk] b_auF[sk]] cos [] needInScope [auD :-> fun_auD[sk], aB4 :-> k_aB4[tau:1]] Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} Presumably this is niteria's in-scope set checks in action. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by niteria): Better trace with `ghc-stage2`: {{{ ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.1.20160128 for x86_64-unknown-linux): ASSERT failed! CallStack (from ImplicitParams): assertPprPanic, called at compiler/types/TyCoRep.hs:1932:51 in ghc:TyCoRep checkValidSubst, called at compiler/types/TyCoRep.hs:1981:17 in ghc:TyCoRep substTys, called at compiler/types/TyCoRep.hs:2002:14 in ghc:TyCoRep substTheta, called at compiler/typecheck/TcPatSyn.hs:254:57 in ghc:TcPatSyn in_scope InScope {k_aB3 k_aB8 a_aB9 b_aBa} tenv [auD :-> a_aB9[tau:5], auE :-> b_aBa[tau:5], aB2 :-> k_aB8[tau:5]] cenv [] tys [fun_auC[sk] ~ a_auD[sk] b_auE[sk]] cos [] needInScope [auC :-> fun_auC[sk], aB3 :-> k_aB3[tau:1]] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: patch Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1879 Wiki Page: | -------------------------------------+------------------------------------- Changes (by niteria): * status: new => patch * differential: => Phab:D1879 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: patch Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1879 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): NB: niteria's (quite necessary) patch does not fix the main issue reported up top. When that patch is merged, we still can't close this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: patch Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1879 Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * keywords: => PatternSynonyms -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures
-------------------------------------+-------------------------------------
Reporter: bgamari | Owner:
Type: bug | Status: patch
Priority: high | Milestone: 8.0.1
Component: Compiler (Type | Version: 8.0.1-rc1
checker) | Keywords:
Resolution: | PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D1879
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Bartosz Nitka
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1879 Wiki Page: | -------------------------------------+------------------------------------- Changes (by niteria): * status: patch => new -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1879 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Could someone fix the pretty-printer (comment:1)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1879, Wiki Page: | Phab:D1896 -------------------------------------+------------------------------------- Changes (by rdragon): * differential: Phab:D1879 => Phab:D1879, Phab:D1896 Comment: See Phab:D1896 for a fix of the pretty-printer. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures
-------------------------------------+-------------------------------------
Reporter: bgamari | Owner:
Type: bug | Status: new
Priority: high | Milestone: 8.0.1
Component: Compiler (Type | Version: 8.0.1-rc1
checker) | Keywords:
Resolution: | PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D1879,
Wiki Page: | Phab:D1896
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1879, Wiki Page: | Phab:D1896 -------------------------------------+------------------------------------- Comment (by bgamari): Merged to `ghc-8.0` as fe7eb57c41739b199a77e460b22d6353b91a14c3. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11524: Something is amiss with quantification in pattern synonym type signatures -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: closed Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: fixed | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1879, Wiki Page: | Phab:D1896 -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11524#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC