Fix #13333 by fixing the covar's type in ctEvCoercion

The change is noted in Note [Given in ctEvCoercion]. This patch
also adds a bit more commentary to TcFlatten, documenting some
key invariants of the flattening algorithm. While in the area,
I also removed some stale commentary from TcCanonical.

6 files changed, 143 insertions, 94 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 2428b6d1a0..10f871f8e9 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -50,85 +50,23 @@ Note [Canonicalization]
 ~~~~~~~~~~~~~~~~~~~~~~~
 
 Canonicalization converts a simple constraint to a canonical form. It is
-unary (i.e. treats individual constraints one at a time), does not do
-any zonking, but lives in TcS monad because it needs to create fresh
-variables (for flattening) and consult the inerts (for efficiency).
-
-The execution plan for canonicalization is the following:
-
-  1) Decomposition of equalities happens as necessary until we reach a
-     variable or type family in one side. There is no decomposition step
-     for other forms of constraints.
-
-  2) If, when we decompose, we discover a variable on the head then we
-     look at inert_eqs from the current inert for a substitution for this
-     variable and contine decomposing. Hence we lazily apply the inert
-     substitution if it is needed.
-
-  3) If no more decomposition is possible, we deeply apply the substitution
-     from the inert_eqs and continue with flattening.
-
-  4) During flattening, we examine whether we have already flattened some
-     function application by looking at all the CTyFunEqs with the same
-     function in the inert set. The reason for deeply applying the inert
-     substitution at step (3) is to maximise our chances of matching an
-     already flattened family application in the inert.
-
-The net result is that a constraint coming out of the canonicalization
-phase cannot be rewritten any further from the inerts (but maybe /it/ can
-rewrite an inert or still interact with an inert in a further phase in the
-simplifier.
-
-Note [Caching for canonicals]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Our plan with pre-canonicalization is to be able to solve a constraint
-really fast from existing bindings in TcEvBinds. So one may think that
-the condition (isCNonCanonical) is not necessary.  However consider
-the following setup:
-
-InertSet = { [W] d1 : Num t }
-WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
-
-Now, we prioritize equalities, but in our concrete example
-(should_run/mc17.hs) the first (d2) constraint is dealt with first,
-because (t ~ Int) is an equality that only later appears in the
-worklist since it is pulled out from a nested implication
-constraint. So, let's examine what happens:
-
-   - We encounter work item (d2 : Num t)
-
-   - Nothing is yet in EvBinds, so we reach the interaction with inerts
-     and set:
-              d2 := d1
-    and we discard d2 from the worklist. The inert set remains unaffected.
-
-   - Now the equation ([W] c : t ~ Int) is encountered and kicks-out
-     (d1 : Num t) from the inerts.  Then that equation gets
-     spontaneously solved, perhaps. We end up with:
-        InertSet : { [G] c : t ~ Int }
-        WorkList : { [W] d1 : Num t}
-
-   - Now we examine (d1), we observe that there is a binding for (Num
-     t) in the evidence binds and we set:
-             d1 := d2
-     and end up in a loop!
-
-Now, the constraints that get kicked out from the inert set are always
-Canonical, so by restricting the use of the pre-canonicalizer to
-NonCanonical constraints we eliminate this danger. Moreover, for
-canonical constraints we already have good caching mechanisms
-(effectively the interaction solver) and we are interested in reducing
-things like superclasses of the same non-canonical constraint being
-generated hence I don't expect us to lose a lot by introducing the
-(isCNonCanonical) restriction.
-
-A similar situation can arise in TcSimplify, at the end of the
-solve_wanteds function, where constraints from the inert set are
-returned as new work -- our substCt ensures however that if they are
-not rewritten by subst, they remain canonical and hence we will not
-attempt to solve them from the EvBinds. If on the other hand they did
-get rewritten and are now non-canonical they will still not match the
-EvBinds, so we are again good.
+unary (i.e. treats individual constraints one at a time).
+
+Constraints originating from user-written code come into being as
+CNonCanonicals (except for CHoleCans, arising from holes). We know nothing
+about these constraints. So, first:
+
+     Classify CNonCanoncal constraints, depending on whether they
+     are equalities, class predicates, or other.
+
+Then proceed depending on the shape of the constraint. Generally speaking,
+each constraint gets flattened and then decomposed into one of several forms
+(see type Ct in TcRnTypes).
+
+When an already-canonicalized constraint gets kicked out of the inert set,
+it must be recanonicalized. But we know a bit about its shape from the
+last time through, so we can skip the classification step.
+
 -}
 
 -- Top-level canonicalization
@@ -1739,7 +1677,7 @@ may reflect the result of unification alpha := ty, so new_pred might
 not _look_ the same as old_pred, and it's vital to proceed from now on
 using new_pred.
 
-The flattener preserves type synonyms, so they should appear in new_pred
+qThe flattener preserves type synonyms, so they should appear in new_pred
 as well as in old_pred; that is important for good error messages.
  -}
 
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 8b3aaa9ebb..dc211c61e4 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -751,6 +751,8 @@ flattenManyNom ev tys
   flatten ty  ==>   (xi, co)
     where
       xi has no type functions, unless they appear under ForAlls
+         has no skolems that are mapped in the inert set
+         has no filled-in metavariables
       co :: xi ~ ty
 
 Note that it is flatten's job to flatten *every type function it sees*.
@@ -761,12 +763,53 @@ Flattening also:
   * applies the substitution embodied in the inert set
 
 Because flattening zonks and the returned coercion ("co" above) is also
-zonked, it's possible that (co :: xi ~ ty) isn't quite true, as ty (the
-input to the flattener) might not be zonked. After zonking everything,
-(co :: xi ~ ty) will be true, however. It is for this reason that we
+zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
+we can rely on these facts:
+  (F1) typeKind(xi) succeeds and returns a fully zonked kind
+  (F2) co :: xi ~ zonk(ty)
+Note that the left-hand type of co is *always* precisely xi. The right-hand
+type may or may not be ty, however: if ty has unzonked filled-in metavariables,
+then the right-hand type of co will be the zonked version of ty.
+It is for this reason that we
 occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
-even before we zonk the whole program. (In particular, this is why the
-zonk in flattenTyVar is necessary.)
+even before we zonk the whole program. For example, see the FTRNotFollowed
+case in flattenTyVar.
+
+Why have these invariants on flattening? Really, they're both to ensure
+invariant (F1), which is a Good Thing because we sometimes use typeKind
+during canonicalisation, and we want this kind to be zonked (e.g., see
+TcCanonical.homogeniseRhsKind). Invariant (F2) is needed solely to support
+(F1). It is relied on in one place:
+
+ - The FTRNotFollowed case in flattenTyVar. Here, we have a tyvar
+ that cannot be reduced any further (that is, no equality over the tyvar
+ is in the inert set such that the inert equality can rewrite the constraint
+ at hand, and it is not a filled-in metavariable).
+ But its kind might still not be flat,
+ if it mentions a type family or a variable that can be rewritten. Flattened
+ types have flattened kinds (see below), so we must flatten the kind. Here is
+ an example:
+
+   let kappa be a filled-in metavariable such that kappa := k.
+   [G] co :: k ~ Type
+
+   We are flattening
+     a :: kappa
+   where a is a skolem.
+
+ We end up in the FTRNotFollowed case, but we need to flatten the kind kappa.
+ Flattening kappa yields (Type, kind_co), where kind_co :: Type ~ k. Note that the
+ right-hand type of kind_co is *not* kappa, because (F1) tells us it's zonk(kappa),
+ which is k. Now, we return (a |> sym kind_co). If we are to uphold (F1), then
+ the right-hand type of (sym kind_co) had better be fully zonked. In other words,
+ the left-hand type of kind_co needs to be zonked... which is precisely what (F2)
+ guarantees.
+
+In order to support (F2), we require that ctEvCoercion, when called on a
+zonked CtEvidence, always returns a zonked coercion. See Note [Given in
+ctEvCoercion]. This requirement comes into play in flatten_tyvar2. (I suppose
+we could move the logic from ctEvCoercion to flatten_tyvar2, but it's much
+easier to do in ctEvCoercion.)
 
 Flattening a type also means flattening its kind. In the case of a type
 variable whose kind mentions a type family, this might mean that the result
@@ -876,7 +919,7 @@ flatten_one (AppTy ty1 ty2)
            (NomEq,  _)                -> flatten_rhs xi1 co1 NomEq
            (ReprEq, Nominal)          -> flatten_rhs xi1 co1 NomEq
            (ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq
-           (ReprEq, Phantom)          ->
+           (ReprEq, Phantom)          -> -- See Note [Phantoms in the flattener]
              do { ty2 <- liftTcS $ zonkTcType ty2
                 ; return ( mkAppTy xi1 ty2
                          , mkAppCo co1 (mkNomReflCo ty2)) } }
@@ -954,8 +997,8 @@ flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
 -- between and then use transitivity. See Note [Flattening coercions]
 flatten_co :: Coercion -> FlatM (Coercion, Coercion)
 flatten_co co
-  = do { let (Pair ty1 ty2, role) = coercionKindRole co
-       ; co <- liftTcS $ zonkCo co  -- squeeze out any metavars from the original
+  = do { co <- liftTcS $ zonkCo co  -- see Note [Zonking when flattening a coercion]
+       ; let (Pair ty1 ty2, role) = coercionKindRole co
        ; (co1, co2) <- flattenKinds $
                        do { (_, co1) <- flatten_one ty1
                           ; (_, co2) <- flatten_one ty2
@@ -999,12 +1042,39 @@ In other words:
   then
       fco :: fs ~r1 ft
       fs, ft are flattened types
-      kco :: (fs ~r1 ft) ~r2 (s ~r1 t)
+      kco :: fco ~r2 co
 
 The second return value of flatten_co is always a ProofIrrelCo. As
 such, it doesn't contain any information the caller doesn't have and
 might not be necessary in whatever comes next.
 
+Note that a flattened coercion might have unzonked metavariables or
+type functions in it -- but its *kind* will not. Instead of just flattening
+the kinds and using mkTransCo, we could actually flatten the coercion
+structurally. But doing so seems harder than simply flattening the types.
+
+Note [Zonking when flattening a coercion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The first step in flatten_co (see Note [Flattening coercions]) is to
+zonk the input. This is necessary because we want to ensure the following
+invariants (c.f. the invariants (F1) and (F2) in Note [Flattening])
+  If
+    (co', kco) <- flatten_co co
+  Then
+    (FC1) coercionKind(co') succeeds and produces a fully zonked pair of kinds
+    (FC2) kco :: co' ~ zonk(co)
+We must zonk to ensure (1). This is because fco is built by using mkTransCo
+to build up on the input co. But if the only action that happens during
+flattening ty1 and ty2 is to zonk metavariables, the coercions returned
+(co1 and co2) will be reflexive. The mkTransCo calls will drop the reflexive
+coercions and co' will be the same as co -- with unzonked kinds.
+
+These invariants are necessary to uphold (F1) and (F2) in the CastTy and
+CoercionTy cases.
+
+We zonk right at the beginning to avoid duplicating work when flattening the
+ty1 and ty2.
+
 Note [Flattening synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 Not expanding synonyms aggressively improves error messages, and
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 4d399e6cbe..ba7c44feba 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1646,9 +1646,9 @@ of (cc_ev ct), and is fully rewritten wrt the substitution.   Eg for CDictCan,
 This holds by construction; look at the unique place where CDictCan is
 built (in TcCanonical).
 
-In contrast, the type of the evidence *term* (ccev_evtm or ctev_evar/dest) in
+In contrast, the type of the evidence *term* (ctev_dest / ctev_evar) in
 the evidence may *not* be fully zonked; we are careful not to look at it
-during constraint solving.  See Note [Evidence field of CtEvidence]
+during constraint solving. See Note [Evidence field of CtEvidence].
 -}
 
 mkNonCanonical :: CtEvidence -> Ct
@@ -2402,6 +2402,16 @@ For Givens we make new EvVars and bind them immediately. Two main reasons:
     (see evTermCoercion), so the easy thing is to bind it to an Id.
 
 So a Given has EvVar inside it rather than (as previously) an EvTerm.
+
+Note [Given in ctEvCoercion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When retrieving the evidence from a Given equality, we update the type of the EvVar
+from the ctev_pred field. In Note [Evidence field of CtEvidence], we claim that
+the type of the evidence is never looked at -- but this isn't true in the case of
+a coercion that is used in a type. (See the comments in Note [Flattening] in TcFlatten
+about the FTRNotFollowed case of flattenTyVar.) So, right here where we are retrieving
+the coercion from a Given, we update the type to make sure it's zonked.
+
 -}
 
 -- | A place for type-checking evidence to go after it is generated.
@@ -2418,7 +2428,6 @@ data TcEvDest
 
 data CtEvidence
   = CtGiven    -- Truly given, not depending on subgoals
-               -- NB: Spontaneous unifications belong here
       { ctev_pred :: TcPredType      -- See Note [Ct/evidence invariant]
       , ctev_evar :: EvVar           -- See Note [Evidence field of CtEvidence]
       , ctev_loc  :: CtLoc }
@@ -2459,9 +2468,11 @@ ctEvTerm :: CtEvidence -> EvTerm
 ctEvTerm ev@(CtWanted { ctev_dest = HoleDest _ }) = EvCoercion $ ctEvCoercion ev
 ctEvTerm ev = EvId (ctEvId ev)
 
+-- Always returns a coercion whose type is precisely ctev_pred of the CtEvidence.
+-- See also Note [Given in ctEvCoercion]
 ctEvCoercion :: CtEvidence -> Coercion
-ctEvCoercion (CtGiven { ctev_evar = ev_id })
-  = mkTcCoVarCo ev_id
+ctEvCoercion (CtGiven { ctev_pred = pred_ty, ctev_evar = ev_id })
+  = mkTcCoVarCo (setVarType ev_id pred_ty)  -- See Note [Given in ctEvCoercion]
 ctEvCoercion (CtWanted { ctev_dest = dest, ctev_pred = pred })
   | HoleDest hole <- dest
   , Just (role, ty1, ty2) <- getEqPredTys_maybe pred
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 05a18705d3..e943254d18 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -1382,6 +1382,7 @@ addInertEq :: Ct -> TcS ()
 addInertEq ct
   = do { traceTcS "addInertEq {" $
          text "Adding new inert equality:" <+> ppr ct
+
        ; ics <- getInertCans
 
        ; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev }) <- maybeEmitShadow ics ct
diff --git a/testsuite/tests/typecheck/should_compile/T13333.hs b/testsuite/tests/typecheck/should_compile/T13333.hs
new file mode 100644
index 0000000000..fba64cede0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13333.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T13333 where
+
+import Data.Data
+import GHC.Exts (Constraint)
+
+data T (phantom :: k) = T
+
+data D (p :: k -> Constraint) (x :: j) where
+  D :: forall (p :: k -> Constraint) (x :: k). p x => D p x
+
+class Possibly p x where
+  possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)
+
+dataCast1T :: forall k c t (phantom :: k).
+              (Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
+           => (forall d. Data d => c (t d))
+           -> Maybe (c (T phantom))
+dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
+                 Nothing -> Nothing
+                 Just D  -> gcast1 f
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 67fe104155..874235387e 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -556,3 +556,4 @@ test('T13524', normal, compile, [''])
 test('T13509', normal, compile, [''])
 test('T13526', normal, compile, [''])
 test('T13603', normal, compile, [''])
+test('T13333', normal, compile, [''])