[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 Simon Peyton Jones <simonpj@…>):

 In [changeset:"0faf7fd3e6c652575af9993787f07cad86f452f6/ghc"
 0faf7fd3/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="0faf7fd3e6c652575af9993787f07cad86f452f6"
 Refactor the treatment of predicate types

 Trac #15648 showed that GHC was a bit confused about the
 difference between the types for

 * Predicates
 * Coercions
 * Evidence (in the typechecker constraint solver)

 This patch cleans it up. See especially Type.hs
 Note [Types for coercions, predicates, and evidence]

 Particular changes

 * Coercion types (a ~# b) and (a ~#R b) are not predicate types
   (so isPredTy reports False for them) and are not implicitly
   instantiated by the type checker.  This is a real change, but
   it consistently reflects that fact that (~#) and (~R#) really
   are different from predicates.

 * isCoercionType is renamed to isCoVarType

 * During type inference, simplifyInfer, we do /not/ want to infer
   a constraint (a ~# b), because that is no longer a predicate type.
   So we 'lift' it to (a ~ b). See TcType
   Note [Lift equality constaints when quantifying]

 * During type inference for pattern synonyms, we need to 'lift'
   provided constraints of type (a ~# b) to (a ~ b).  See
   Note [Equality evidence in pattern synonyms] in PatSyn

 * But what about (forall a. Eq a => a ~# b)? Is that a
   predicate type?  No -- it does not have kind Constraint.
   Is it an evidence type?  Perhaps, but awkwardly so.

   In the end I decided NOT to make it an evidence type,
   and to ensure the the type inference engine never
   meets it.  This made me /simplify/ the code in
   TcCanonical.makeSuperClasses; see TcCanonical
   Note [Equality superclasses in quantified constraints]

   Instead I moved the special treatment for primitive
   equality to TcInteract.doTopReactOther.  See TcInteract
   Note [Looking up primitive equalities in quantified constraints]

   Also see Note [Evidence for quantified constraints] in Type.

   All this means I can have
      isEvVarType ty = isCoVarType ty || isPredTy ty
   which is nice.

 All in all, rather a lot of work for a small refactoring,
 but I think it's a real improvement.
 }}}

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