[GHC] #15799: GHC panic (and warnings)

[GHC]

#15799: GHC panic (and warnings)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12045            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Urgh. I know what's going on. It has nothing to do with #12045, but
 perhaps changes there affected code paths in such a way that this
 surfaced.

 The problem is that we have a constraint `b <= a`. Note that `(<=) :: ty1
 -> ty2 -> Type` -- that is, `b <= a` is ill-kinded as a constraint. So GHC
 processes it and dutifully wraps it up by casting by a coercion hole; we
 get `(b <= a) |> co`, where `co :: Type ~ Constraint`. Then, we zonk (with
 `zonkTcType`). The zonker uses `mapType` with `tcm_smart` set to `True`.
 This means that casts are reconstructed with `mkCastTy`, which, of course,
 does a reflexivity check. And, lo, the reflexivity check decides that
 `Type` and `Constraint` are equal and thus drops the cast. Later, we try
 to treat `b <= a` as an predicate, and GHC falls over when `isPredTy (b <=
 a)` returns `False`.

 What to do? My first instinct was to add a new setting to `tcm_smart`:
 sometimes we want to use raw constructors (in `nakedSubstMapper`),
 sometimes we want core smart constructors (in `zonkTcTypeToType`), and now
 sometimes we want type-checker smart constructors (newly discovered for
 `zonkTcType`). We'll also need a `mkTcCastTy` which is like `mkCastTy` but
 calls `isTcReflexiveCo` instead of `isReflexiveCo`, so that `Type` can be
 known to be distinct from `Constraint`. (Actually, `mkTcCastTy` can
 probably skip some of the steps in `mkCastTy`, as we know we'll get
 another crack at establishing invariants, etc., in `zonkTcTypeToType`.)

 This is a mess! So my second instinct was to post here for help. Help?
 Does anyone see a way out?

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15799#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler