[commit: ghc] master: Refactor the treatment of predicate types (0faf7fd)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/0faf7fd3e6c652575af9993787f07cad86f452f6/ghc

>---------------------------------------------------------------

commit 0faf7fd3e6c652575af9993787f07cad86f452f6
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Oct 16 12:38:16 2018 +0100

    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.


>---------------------------------------------------------------

0faf7fd3e6c652575af9993787f07cad86f452f6
 compiler/basicTypes/Id.hs                          | 18 ++---
 compiler/coreSyn/CoreLint.hs                       |  4 +-
 compiler/coreSyn/CoreOpt.hs                        |  2 +-
 compiler/coreSyn/CoreUtils.hs                      |  2 +-
 compiler/deSugar/DsBinds.hs                        |  6 +-
 compiler/typecheck/ClsInst.hs                      |  7 +-
 compiler/typecheck/TcCanonical.hs                  | 56 ++++++--------
 compiler/typecheck/TcErrors.hs                     |  4 +-
 compiler/typecheck/TcEvidence.hs                   |  6 +-
 compiler/typecheck/TcInteract.hs                   | 44 ++++++++++-
 compiler/typecheck/TcPatSyn.hs                     | 60 ++++++++++++++-
 compiler/typecheck/TcType.hs                       | 89 +++++++++++++++-------
 compiler/types/TyCoRep.hs                          | 13 +---
 compiler/types/Type.hs                             | 79 ++++++++++++++++---
 .../partial-sigs/should_compile/T15039c.stderr     |  4 +-
 .../partial-sigs/should_compile/T15039d.stderr     |  5 +-
 .../tests/typecheck/should_fail/T13320.stderr      |  3 +-
 17 files changed, 282 insertions(+), 120 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc 0faf7fd3e6c652575af9993787f07cad86f452f6