#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