[GHC] #15648: Core Lint error with source-level unboxed equality

[GHC]

#15648: Core Lint error with source-level unboxed equality
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15209            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I can see several things here.

 1. `(~#)` has a funny kind (see `prelude/TysPrim`:
 {{{
 (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep [])
 }}}
   The kind `TYPE TupleRep []` says that values of this type are
 represented by a zero-tuple of values; which takes zero bits.

 2.  Note that it does ''not'' have return kind `Constraint`.  Indeed, it
 can't, because that would mean it had a boxed, lifted representation,
 since (after the type checker) `Constraint` and `Type` are the same.  So
 it won't behave like an invisible argument, because it doesn't have kind
 `Constraint`.  Making `(~#)` behave like `(~)` in source code would be
 problematic for this reason.

 3.  In Core, term-level variables (`Id`) are split into coercion variables
 (`CoVar`s) and all others; distinguished by their `IdDetails` field, and
 `isCoVarId`.  Coercion variables can be ''bound'' in terms (say by a
 lambda) but, unlike other Ids, can ''occur'' only in types and coercions.
 The simplifier keeps them in a different environment for that reason.  In
 short:

   * A variable should reply True to `isCoVarId` '''iff''' it has type `t1
 ~# t2` or `t1 ~R# t2`.
   * A `CoVar` should occur only in types or coercions, never in a term
 (i.e. `Var` in Core).

   Lint checks for the latter, but not the former; I'll fix that.

 4. This program has a non-`CoVar` bound by a lambda, and that's why the
 simplifier is breaking.

 TL;DR: there a shortcoming in Lint, which I'll fix.   Beyond that, GHC
 should really give a better error than a Lint failure in this case, but
 it's a bit exotic, and I'm not really sure where the best place to do it
 is.  Maybe `chekcValidType`?

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