[GHC] #15918: GHC panic from QuantifiedConstraints(?)

[GHC]

#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