[GHC] #15918: GHC panic from TypeApplications(?)
#15918: GHC panic from TypeApplications(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash. {{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-} import Data.Kind class Rev f where rev :: f a instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined data Build :: ((k -> Type) -> Constraint) -> (k -> Type) uu = rev :: Build [] a }}} gives a panic {{{ $ ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from TypeApplications(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash.
{{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-}
import Data.Kind
class Rev f where rev :: f a
instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined
data Build :: ((k -> Type) -> Constraint) -> (k -> Type)
uu = rev :: Build [] a }}}
gives a panic
{{{ $ ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
New description: Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash. {{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-} import Data.Kind class Rev f where rev :: f a instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined data Build :: ((k -> Type) -> Constraint) -> (k -> Type) uu = rev :: Build [] a }}} gives a panic {{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints 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 goldfire): * keywords: TypeApplications => QuantifiedConstraints Comment: I don't see anything involving type applications here. Changing ticket accordingly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): This is another symptom of the bug identified in #15799. In the example of this ticket we have {{{ Elaborated types Rev :: forall k. (k->*) -> Constraint Build :: forall k. ((k->*) -> Constraint) -> k -> * rev :: forall k (f :: k->*) (a :: k). Rev @k f => f a instance forall k (cls :: (k->*) -> Constraint). (forall (xx :: k->*). cls xx => Rev @k xx) => Rev @k (Build @k cls) From the RHS of uu: [W] Rev @k (Build ([] |> co)) [W] co :: (* -> *) ~ ((k->*) -> Constraint) }}} Decompose co, we get {{{ [W] Rev @k (Build ([] |> (co1 -> co2))) [W] co1 :: * ~ (k->*) [W] co2 :: * ~ Constraint }}} Now the first constraint matches the instance, so we get a substitution: {{{ cls :-> ([] |> (co1 -> co2) }}} Now * we apply `substTheta` (this is in `Inst.instDFunType`) to `(cls xx)` * `substTheta` calls `mkAppTy ([] |> (co1 -> co2)) xx` * `mkAppTy` uses `decomposePiCos` (which works) and then calls `mkCastTy` (twice) * Alas, `mkCastTy` considers that `Constraint ~ *`, and we lose `co2` And that's how the assert fails. The underlying cause is the same: `mkCastTy` is using `isReflexiveCo`, and we really want `mkTcCastTy` here. But we don't really want to have a `Tc` variant of `substTy`! Sigh. So much pain from the varying treatment of `Constraint` and `Type`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I propose to fix this by making `mkCastTy` use `isReflCo` rather than `isReflexiveCo`. That way it will get rid of simple reflexive casts produced by the unifier, but will not remove compound `ty ~ ty` casts. That will happen in `OptCoercion`. This is a bit more efficient (less `tcEqType`) and it comopletely avoids this horrible constraint/type choice, meaning that `substTy`, `mkCastTy` and `mkAppTy` can all be used both by Core and by the type checker. Richard: do you agree? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think that's problematic. See the comments around that use of `isReflexiveCo`. Perhaps there is a way to avoid it, but there is a good principled reason around the use of the slower function. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
See the comments around that use of isReflexiveCo.
Which comments? I think you may be referring to `Note [Respecting definitional equality]` in `TyCoRep`. Anything else? Let me also note that * In GHC today we use `mkNakedCastTy` which absolutely does not remove the casts that the above `Note` says it should. * The typechecker is careful to push casts out of the way when solving equalities, which helps. But it still has lots of `tcSplitX` calls.
I think that's problematic.
What do you suggest we do? As comment:3 shows, if we have `mkTcCastTy` we'll need `mkTcAppTy`. And `tcSubstTy` and `tcSubstTheta`. And `tcInstDFunType`. It's pretty hard to be sure that we've nailed all the places. Duplicating all this stuff doesn't smell right to me. Hmm. Currently `mkCastTy` will remove a cast between `Type` and `Coercion`, because the two are equal in Core. But such a cast would yield a typechecker error (which is what both #15799 and this ticket involve), so we'd never get as far as Core. How bad would it be if `mkCastTy` did not remove a cast between `Type` and `Coercion`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I do mean that note, and also the NB comment right after the call to `isReflexiveCo`. You're right about the `mkNakedCastTy`. There could be a latent bug there, because `tcSplitTyConApp` won't work as it should if a cast makes a `TyConApp` look like something else.
How bad would it be if `mkCastTy` did not remove a cast between `Type` and `Coercion`?
It's potentially bad. Suppose we have `tyco :: Type ~ Coercion`. Then `Bool |> tyco` is `eqType` to `Bool`, but `splitTyConApp` behaves differently on them. Here's another approach: what if `coreView` dispenses with reflexive coercions, not `mkCastTy`? We're already careful to use `coreView` liberally. Implemented correctly, this should satisfy the definitional equality concerns. The problem will be performance: it's potentially expensive to check coercion types and compute equality, and `coreView` is called a lot. (Specifically, it's a shame to build a cast only to have to remove it lots of times.) But maybe we could take a hybrid approach: `mkCastTy` discards reflexive coercions that aren't `Type`-vs-`Coercion`, and `coreView` discards the rest. (`tcView` wouldn't, of course!) That would work, I think, but I'm not in love with the approach. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
also the NB comment right after the call to isReflexiveCo.
To be explicit, you mean {{{ mkCastTy :: Type -> Coercion -> Type mkCastTy ty co | isReflexiveCo co = ty -- (EQ2) from the Note -- NB: Do the slow check here. This is important to keep the splitXXX -- functions working properly. Otherwise, we may end up with something -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz) -- fails under splitFunTy_maybe. This happened with the cheaper check -- in test dependent/should_compile/dynamic-paper. }}}
Suppose we have tyco :: Type ~ Coercion
It's worth noting that the type checker will produce an error message for any such coercion. It's like `Int ~ Bool`. I feel somewhat relaxed about the impact on Core of not upholding an equality that will be rejected by the typechecker anyway. (Long term I think we probably want to make Type and Coercion distinct everywhere.)
mkCastTy discards reflexive coercions that aren't Type-vs-Coercion, and coreView discards the rest
Hm. You mean something like {{{ tcView (ty |> co) | ty1 == coercionKind, ty2 == typeKind = Just ty | ty1 = typeKind, ty2 == coercionKind = Just ty where (ty1,ty2) = coercionKind co }}} I suppose that'd be possible. But I agree it's smelly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The type-checker might conceivably not produce an error for a coercion like that. For example, if we have {{{#!hs class Def a where meth :: a }}} then we get `axDef :: Def a ~R# a`, and thus `KindCo axDef :: Constraint ~# Type`. Would this happen in practice? Most likely not, but we can't rule it out. One possible route is to have `mkCastTy` carefully not discard `Type`/`Constraint` coercions... and do nothing else. This would violate property `(EQ)` of `Note [Non-trivial definitional equality]`. But (assuming the type-checker never maliciously produces `KindCo axDef`), this would come up only in ill-typed programs. Still, I can't rule out the possibility of a panic or poor error message in such a scenario. Perhaps worse, any misbehavior would be terribly fragile, based as it would be on an arbitrary choice between two things that GHC thinks are equal. As we're thinking about this, it's not just coercions between `Type` and `Constraint` that are in play: it's all coercions that are reflexive except for variations between `Type` and `Constraint`. For example, a coercion between `Type -> Constraint` and `Type -> Type`. So the simplistic check proposed in comment:9 would be insufficient. One other possible solution: introduce a `TcCastTy :: Type -> Coercion -> Type` constructor in `Type`, with the following invariant: the coercion stored is reflexive in Core but irreflexive in Haskell. That is, the coercion would relate something that mentions `Type` to something that mentions `Constraint`. `mkCastTy` could cleverly figure out whether to make a `CastTy` or a `TcCastTy`. `coreView` could discard `TcCastTy`s; `tcView` wouldn't. This is similar to the plan Simon expands in comment:9, but caching the decision of whether to discard. It's still all a bit distasteful, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This appears to no longer happen on a recent `devel2`-flavoured GHC HEAD: {{{ GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( ../Bug.hs, interpreted ) ../Bug.hs:18:19: error: • Expected kind ‘(k0 -> *) -> Constraint’, but ‘[]’ has kind ‘* -> *’ • In the first argument of ‘Build’, namely ‘[]’ In an expression type signature: Build [] a In the expression: rev :: Build [] a | 18 | uu = rev :: Build [] a | ^^ }}} Should we add a test case for this and call it fixed? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?)
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.6.2
Resolution: | Keywords:
| QuantifiedConstraints
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/489 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => https://gitlab.haskell.org/ghc/ghc/merge_requests/489 Comment: https://gitlab.haskell.org/ghc/ghc/merge_requests/489 follows up on comment:11 by adding a regression test. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: fixed | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T15918 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/489 -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => quantified-constraints/T15918 * status: patch => closed * resolution: => fixed Comment: Regression test landed in https://gitlab.haskell.org/ghc/ghc/commit/db039a4a10fc8fa9e03e6781d1c0dc3315... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.2 Resolution: fixed | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T15918 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/489 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: => 8.10.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: GHC panic from QuantifiedConstraints(?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T15918 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/489 -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * resolution: fixed => Comment: Actually on second thoughts I cannot recall our Plan for `mkCastTy`, so I'm not sure this problem is truly fixed. Maybe it's just harder to trigger now! Let's see what Richard remembers. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: mkCastTy sometimes drops insoluble (Type ~ Constraint) coercions -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T15918 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/489 -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: QuantifiedConstraints => * milestone: 8.10.1 => ⊥ Old description:
Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash.
{{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-}
import Data.Kind
class Rev f where rev :: f a
instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined
data Build :: ((k -> Type) -> Constraint) -> (k -> Type)
uu = rev :: Build [] a }}}
gives a panic
{{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
New description: EDIT: See comment:3 for the real cause and comment:17 for the current plan. --------------------------- Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash. {{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-} import Data.Kind class Rev f where rev :: f a instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined data Build :: ((k -> Type) -> Constraint) -> (k -> Type) uu = rev :: Build [] a }}} gives a panic {{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- Comment: I think we decided to punt. comment:11 reports that the original bug is fixed. In addition, this ticket's friend #15799 is also no longer triggering. So I think the underlying bug here is real, but it's both difficult (impossible?) to trigger and difficult to fix. Furthermore, the bug can only strike in ''incorrect'' programs. This bug ''cannot'' make ill-typed Core. All of this suggests that we take my personal favorite course of action: do nothing. I've retitled the ticket to be more informative and will set the milestone accordingly. But I don't quite want to close the ticket, because I do believe there is a real bug here. Perhaps someday we'll find a way to trigger this ticket, making it more worthwhile to invest in a fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: mkCastTy sometimes drops insoluble (Type ~ Constraint) coercions
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: ⊥
Component: Compiler | Version: 8.6.2
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case: quantified-
| constraints/T15918
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/489
-------------------------------------+-------------------------------------
Comment (by Marge Bot
#15918: mkCastTy sometimes drops insoluble (Type ~ Constraint) coercions -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T15918 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/489 -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
EDIT: See comment:3 for the real cause and comment:17 for the current plan. ---------------------------
Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash.
{{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-}
import Data.Kind
class Rev f where rev :: f a
instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined
data Build :: ((k -> Type) -> Constraint) -> (k -> Type)
uu = rev :: Build [] a }}}
gives a panic
{{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
New description: '''EDIT: See comment:3 for the real cause and comment:17 for the current plan.''' See also: * TyCoRep `Note [Respecting definitional equality]` and its supporting `Note [Non-trivial definitional equality]` * #11715 Constraint vs * * #15799 TL;DR: there's a bug in here, that we don't know how to solve. But it's not biting us, and once we solve #11715 that may point the way. --------------------------- Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash. {{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-} import Data.Kind class Rev f where rev :: f a instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined data Build :: ((k -> Type) -> Constraint) -> (k -> Type) uu = rev :: Build [] a }}} gives a panic {{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15918: mkCastTy sometimes drops insoluble (Type ~ Constraint) coercions -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: ⊥ Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: quantified- | constraints/T15918 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/489 -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
'''EDIT: See comment:3 for the real cause and comment:17 for the current plan.'''
See also: * TyCoRep `Note [Respecting definitional equality]` and its supporting `Note [Non-trivial definitional equality]` * #11715 Constraint vs * * #15799
TL;DR: there's a bug in here, that we don't know how to solve. But it's not biting us, and once we solve #11715 that may point the way.
---------------------------
Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash.
{{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-}
import Data.Kind
class Rev f where rev :: f a
instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined
data Build :: ((k -> Type) -> Constraint) -> (k -> Type)
uu = rev :: Build [] a }}}
gives a panic
{{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
New description: '''EDIT: See comment:3 for the real cause and comment:17 for the current plan.''' See also: * TyCoRep `Note [Respecting definitional equality]` and its supporting `Note [Non-trivial definitional equality]` * #11715 Constraint vs * * #15799 * #13650 TL;DR: there's a bug in here, that we don't know how to solve. But it's not biting us, and once we solve #11715 that may point the way. --------------------------- Minimized from https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I don't expect `Build []` to kind check but ti shouldn't crash. {{{#!hs {-# Language PolyKinds #-} {-# Language TypeFamilies #-} {-# Language ConstraintKinds #-} {-# Language FlexibleContexts #-} {-# Language QuantifiedConstraints #-} {-# Language UndecidableInstances #-} import Data.Kind class Rev f where rev :: f a instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where rev = undefined data Build :: ((k -> Type) -> Constraint) -> (k -> Type) uu = rev :: Build [] a }}} gives a panic {{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ~/hs/711_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in ghc:TcType Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15918#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC