Allow (~) in the head of a quantified constraints

Since the introduction of quantified constraints, GHC has rejected
a quantified constraint with (~) in the head, thus
  f :: (forall a. blah => a ~ ty) => stuff

I am frankly dubious that this is ever useful.  But /is/ necessary for
Coercible (representation equality version of (~)) and it does no harm
to allow it for (~) as well.  Plus, our users are asking for it
(Trac #15359, #15625).

It was really only excluded by accident, so
this patch lifts the restriction. See TcCanonical
Note [Equality superclasses in quantified constraints]

There are a number of wrinkles:

* If the context of the quantified constraint is empty, we
  can get trouble when we get down to unboxed equality (a ~# b)
  or (a ~R# b), as Trac #15625 showed. This is even more of
  a corner case, but it produced an outright crash, so I elaborated
  the superclass machinery in TcCanonical.makeStrictSuperClasses
  to add a void argument in this case.  See
  Note [Equality superclasses in quantified constraints]

* The restriction on (~) was in TcValidity.checkValidInstHead.
  In lifting the restriction I discovered an old special case for
  (~), namely
      | clas_nm `elem` [ heqTyConName, eqTyConName]
      , nameModule clas_nm /= this_mod
  This was (solely) to support the strange instance
      instance a ~~ b => a ~ b
  in Data.Type.Equality. But happily that is no longer
  with us, since
     commit f265008fb6f70830e7e92ce563f6d83833cef071
     Refactor (~) to reduce the suerpclass stack
  So I removed the special case.

* I found that the Core invariants on when we could have
       co = <expr>
  were entirely not written down. (Getting this wrong ws
  the proximate source of the crash in Trac #15625.  So

  - Documented them better in CoreSyn
      Note [CoreSyn type and coercion invariant],
  - Modified CoreOpt and CoreLint to match
  - Modified CoreUtils.bindNonRec to match
  - Made MkCore.mkCoreLet use bindNonRec, rather
    than duplicate its logic
  - Made Simplify.rebuildCase case-to-let respect
      Note [CoreSyn type and coercion invariant],

1 files changed, 21 insertions, 14 deletions

diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 8a41c98822..3254d7334c 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -32,7 +32,7 @@ import PprCore  ( pprCoreBindings, pprRules )
 import OccurAnal( occurAnalyseExpr, occurAnalysePgm )
 import Literal  ( Literal(MachStr) )
 import Id
-import Var      ( varType )
+import Var      ( varType, isNonCoVarId )
 import VarSet
 import VarEnv
 import DataCon
@@ -360,7 +360,10 @@ simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst })
   = ASSERT( isCoVar in_bndr )
     (env { soe_subst = extendCvSubst subst in_bndr out_co }, Nothing)
 
-  | pre_inline_unconditionally
+  | ASSERT2( isNonCoVarId in_bndr, ppr in_bndr )
+    -- The previous two guards got rid of tyvars and coercions
+    -- See Note [CoreSyn type and coercion invariant] in CoreSyn
+    pre_inline_unconditionally
   = (env { soe_inl = extendVarEnv inl_env in_bndr clo }, Nothing)
 
   | otherwise
@@ -385,12 +388,11 @@ simple_bind_pair env@(SOE { soe_inl = inl_env, soe_subst = subst })
 
     pre_inline_unconditionally :: Bool
     pre_inline_unconditionally
-       | isCoVar in_bndr          = False    -- See Note [Do not inline CoVars unconditionally]
-       | isExportedId in_bndr     = False    --     in SimplUtils
+       | isExportedId in_bndr     = False
        | stable_unf               = False
        | not active               = False    -- Note [Inline prag in simplOpt]
        | not (safe_to_inline occ) = False
-       | otherwise = True
+       | otherwise                = True
 
         -- Unconditionally safe to inline
     safe_to_inline :: OccInfo -> Bool
@@ -423,7 +425,10 @@ simple_out_bind_pair :: SimpleOptEnv
                      -> (SimpleOptEnv, Maybe (OutVar, OutExpr))
 simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
                      occ_info active stable_unf
-  | post_inline_unconditionally
+  | ASSERT2( isNonCoVarId in_bndr, ppr in_bndr )
+    -- Type and coercion bindings are caught earlier
+    -- See Note [CoreSyn type and coercion invariant]
+    post_inline_unconditionally
   = ( env' { soe_subst = extendIdSubst (soe_subst env) in_bndr out_rhs }
     , Nothing)
 
@@ -437,14 +442,16 @@ simple_out_bind_pair env in_bndr mb_out_bndr out_rhs
 
     post_inline_unconditionally :: Bool
     post_inline_unconditionally
-       | not active                  = False
-       | isWeakLoopBreaker occ_info  = False -- If it's a loop-breaker of any kind, don't inline
-                                             -- because it might be referred to "earlier"
-       | stable_unf                  = False -- Note [Stable unfoldings and postInlineUnconditionally]
-       | isExportedId in_bndr        = False -- Note [Exported Ids and trivial RHSs]
-       | exprIsTrivial out_rhs       = True
-       | coercible_hack              = True
-       | otherwise                   = False
+       | isExportedId in_bndr  = False -- Note [Exported Ids and trivial RHSs]
+       | stable_unf            = False -- Note [Stable unfoldings and postInlineUnconditionally]
+       | not active            = False --     in SimplUtils
+       | is_loop_breaker       = False -- If it's a loop-breaker of any kind, don't inline
+                                       -- because it might be referred to "earlier"
+       | exprIsTrivial out_rhs = True
+       | coercible_hack        = True
+       | otherwise             = False
+
+    is_loop_breaker = isWeakLoopBreaker occ_info
 
     -- See Note [Getting the map/coerce RULE to work]
     coercible_hack | (Var fun, args) <- collectArgs out_rhs