Introduce InstanceOfRefl evidence to match description

6 files changed, 46 insertions, 26 deletions

diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 5ff14fe3c2..340b1574a7 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -1195,6 +1195,8 @@ applyInstanceOf id e
   = pprPanic "The impossible happened" (ppr id)
 
 dsEvInstanceOf :: EvInstanceOf -> CoreExpr -> DsM CoreExpr
+dsEvInstanceOf EvInstanceOfRefl e
+  = return e
 dsEvInstanceOf (EvInstanceOfEq co) e
   = do { dsTcCoercion co $ \c ->
            case coercionKind c of
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 169faee58d..433971ec40 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1693,7 +1693,11 @@ can_instance_of :: Ct -> TcS (StopOrContinue Ct)
 can_instance_of (CInstanceOfCan { cc_ev = ev, cc_lhs = lhs, cc_rhs = rhs })
     -- case InstanceOf sigma sigma, for the exact same sigma
   | lhs `eqType` rhs
-  = can_instance_to_eq ev lhs rhs
+  = case ev of
+      CtWanted { ctev_evar = evar } ->
+        do { setWantedEvBind evar (mkInstanceOfRefl lhs)
+           ; stopWith ev "can_instance_of/REFL" }
+      _ -> stopWith ev "Given/Derived instanceOf instantiation"
     -- case InstanceOf ty (forall qvars. Q => ty)
   | is_forall rhs
   = case ev of
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index a1984f52c6..9b4d132505 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -18,7 +18,8 @@ module TcEvidence (
   EvLit(..), evTermCoercion,
   EvCallStack(..),
   EvTypeable(..),
-  EvInstanceOf(..), mkInstanceOfEq, mkInstanceOfInst, mkInstanceOfGen,
+  EvInstanceOf(..), mkInstanceOfRefl, mkInstanceOfEq,
+  mkInstanceOfInst, mkInstanceOfGen,
 
   -- TcCoercion
   TcCoercion(..), TcCoercionR, TcCoercionN,
@@ -780,21 +781,27 @@ data EvCallStack
 {- Note [Evidence for InstanceOf constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
+             g : t ~N t
+    --------------------------
+    EvInstanceOfRefl : t <~ t
+
              g : s ~N t
     --------------------------
-    EvInstanceOfEq g : s <= t
+    EvInstanceOfEq g : s <~ t
 
-                 g : (s[tys/as] <= t),   vi : ci[tys/as]
+                 g : (s[tys/as] <~ t),   vi : ci[tys/as]
     -------------------------------------------------------------------------
-    EvInstanceOfInst [t1..tm] g [v1..vn] : (forall a1..am., c1..ck => s) <= t
+    EvInstanceOfInst [t1..tm] g [v1..vn] : (forall a1..am., c1..ck => s) <~ t
 
-                 forall [a1..an]. [v1:c1,..vn:cn] <binds>. g : s <= t
+                 forall [a1..an]. [v1:c1,..vn:cn] <binds>. g : s <~ t
     -------------------------------------------------------------------------
-    EvInstanceOfGen [a1..an] [v1..vn] <binds> g : s <= (forall a1..am., c1..ck => t)
+    EvInstanceOfGen [a1..an] [v1..vn] <binds> g : s <~ (forall a1..am., c1..ck => t)
 -}
 
 data EvInstanceOf
-  = EvInstanceOfEq   TcCoercion  -- ^ term witnessing equality
+  = EvInstanceOfRefl
+
+  | EvInstanceOfEq   TcCoercion  -- ^ term witnessing equality
 
   | EvInstanceOfInst [Type]      -- ^ type variables to apply
                      EvId        -- ^ witness for inner instantiation
@@ -807,6 +814,10 @@ data EvInstanceOf
 
     deriving ( Data.Data, Data.Typeable )
 
+mkInstanceOfRefl :: Type -> EvTerm
+mkInstanceOfRefl ty
+  = EvInstanceOf ty EvInstanceOfRefl
+
 mkInstanceOfEq :: Type -> TcCoercion -> EvTerm
 mkInstanceOfEq ty co
   = EvInstanceOf ty (EvInstanceOfEq co)
@@ -1082,6 +1093,7 @@ evVarsOfTypeable ev =
 evVarsOfInstanceOf :: EvInstanceOf -> VarSet
 evVarsOfInstanceOf ev =
   case ev of
+    EvInstanceOfRefl        -> emptyVarSet
     EvInstanceOfEq   co     -> coVarsOfTcCo co
     EvInstanceOfInst _ co q -> unitVarSet co `unionVarSet` evVarsOfTerms q
     EvInstanceOfGen  _ qvars (EvBinds bs) co ->
@@ -1185,6 +1197,7 @@ instance Outputable EvTypeable where
 instance Outputable EvInstanceOf where
   ppr ev =
     case ev of
+      EvInstanceOfRefl     -> ptext (sLit "REFL")
       EvInstanceOfEq   co  -> ptext (sLit "EQ")   <+> ppr co
       EvInstanceOfInst vars co q
         -> ptext (sLit "INST") <+> ppr vars <+> ppr q <+> ppr co
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index a6c783b077..9ca25b75ae 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1328,6 +1328,8 @@ zonkEvBind env (EvBind { eb_lhs = var, eb_rhs = term, eb_is_given = is_given })
       ; return (EvBind { eb_lhs = var', eb_rhs = term', eb_is_given = is_given }) }
 
 zonkEvInstanceOf :: ZonkEnv -> EvInstanceOf -> TcM EvInstanceOf
+zonkEvInstanceOf _ EvInstanceOfRefl
+  = return EvInstanceOfRefl
 zonkEvInstanceOf env (EvInstanceOfEq co)
   = do { co' <- zonkTcCoToCo env co
        ; return (EvInstanceOfEq co') }
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 7f8fec6156..5ab11b03fb 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1166,12 +1166,11 @@ data Ct
     }
 
   | CInstanceOfCan {  -- Canonical instance constraints
-       -- InstanceOf constraints are written  s1 <= s2
+       -- InstanceOf constraints are written  s1 <~ s2
        -- pronounced "s1 is more polymorphic than s2"
        --         of "s2 is an instance of s1"
-       -- A /canonical/ InstanceOf constraint has a tyvar the LHS or RHS
-       --    * tyvar <= sigma
-       --    * sigma <= tyvar
+       -- A /canonical/ InstanceOf constraint has a tyvar the LHS
+       --    * sigma <~ tyvar
        --
        -- For now at least, they are always Wanted, never Given/Derived
       cc_ev     :: CtEvidence,
diff --git a/docs/types/impredicativity.ltx b/docs/types/impredicativity.ltx
index d5981ed384..8d3eecbb60 100644
--- a/docs/types/impredicativity.ltx
+++ b/docs/types/impredicativity.ltx
@@ -96,11 +96,12 @@ $$
 $$
 \begin{array}{lrcl}
 \textsc{[$\leq$refl]} & canon\left[\sigma \leq \sigma\right] & = & \epsilon \\
-\textsc{[$\leq$lcon]} & canon\left[\psi_1 \leq \sigma_2\right] & = & \psi_1 \sim \sigma_2 \\
-\textsc{[$\leq$l$\forall$var]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow v) \leq \psi_2 \right] & = & [\overline{a \mapsto \alpha}]v \sim \psi_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
-& & & \textrm{where } v \textrm{ is a unification variable and } v \in \overline{a} \\
+\textsc{[$\leq$lcon]} & canon\left[\sigma_1 \leq \sigma_2\right] & = & \sigma_1 \sim \sigma_2 \\
+& & & \textrm{where } \sigma_1 \not\equiv \sigma_2, \sigma_1 \not\equiv \forall \overline{a}. Q \Rightarrow \sigma'_1 \\
+% \textsc{[$\leq$l$\forall$var]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow v) \leq \psi_2 \right] & = & [\overline{a \mapsto \alpha}]v \sim \psi_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
+% & & & \textrm{where } v \textrm{ is a unification variable and } v \in \overline{a} \\
 \textsc{[$\leq$l$\forall$]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow \sigma_1) \leq \psi_2\right] & = & [\overline{a \mapsto \alpha}]\sigma_1 \leq \sigma_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
-& & & \textrm{where } v \textrm{ is not a unification variable or } v \not\in \overline{a} \\
+% & & & \textrm{where } v \textrm{ is not a unification variable or } v \not\in \overline{a} \\
 \textsc{[$\leq$r$\forall$]} & canon\left[\sigma_1 \leq (\forall \overline{a}. Q_2 \Rightarrow \sigma_2)\right] & = & \forall \overline{a}. \, (Q_2 \supset \sigma_1 \leq \sigma_2) \\
 \end{array}
 $$
@@ -110,7 +111,7 @@ $$
 
 A subset of the canonicalization rules is given in Figures \ref{fig:sim} and \ref{fig:leq}. The only missing ones are those related to flattening of constraints.
 
-\subsubsection*{Notes on the {\sc [$\leq$l$\forall$var]} and {\sc [$\leq$l$\forall$]} rules}
+\subsubsection*{Notes on the {\sc [$\leq$lcon]} and {\sc [$\leq$l$\forall$]} rules}
 
 \begin{itemize}
 \item We disallow applying these rules in the case of unification variables in the right-hand side. If we did so, and later that variable was substituted by some other type, we would need to remember the instantiation done by this rule and apply it to the substituted value. Instead, we prefer to defer the instantiation of the constraint until the variable is changed to another type. The same reasoning applies to disallow application of the rule when the right-hand side is a type family.
@@ -124,7 +125,11 @@ the only constraint being generated is $(\forall\, a.\, \textit{Monoid} \; a \Ri
 
 \item We also disallow applying the rules to quantified types. In that case, we want to apply {\sc [$\leq$r$\forall$]} first, which may in turn lead to an application of the other rules inside the implication.
 
-\item Consider the following code, taken from the {\tt GHC.List} module:
+\item Previously, these rules along with generation and propagation worked very hard to ensure that no constraint of the form $\alpha \leq \sigma$, with $\alpha$ a unification variable, was ever produced.
+
+Nonetheless, there was still the chance that $\alpha \leq \sigma$ is produced from a constraint involving a type family $\mathsf{F} \; \alpha \leq \sigma$ whose family resolves to a variable $\mathsf{F} \; \alpha \sim \alpha$. Since we do not want to loose confluence, we ensure that this resolves to $\alpha \sim \sigma$ regardless of the order of application of rule {\sc [$\leq$lcon]} and type family rewriting.
+
+Furthermore, rule {\sc [$\leq$lcon]} is key in not getting stuck in some programs. Consider the following code, taken from the {\tt GHC.List} module:
 \begin{verbatim}
 head :: [a] -> a
 head (x:xs) = x
@@ -133,11 +138,9 @@ head []     = badHead
 badHead :: b
 badHead = error "..."
 \end{verbatim}
-When type checking the second branch, we generate a constraint of the form $\forall b. b \leq a$. If we were to apply rule {\sc [$\leq$l$\forall$]}, we would get a constraint $\beta \leq a$, getting stuck. Instead, the have the rule {\sc [$\leq$l$\forall$var]}, which ensures that the generated constraint is $\beta \sim a$.
+When type checking the second branch, we generate a constraint of the form $\forall b. b \leq a$. When we apply rule {\sc [$\leq$l$\forall$]}, we get a constraint $\beta \leq a$. If we could not apply {\sc [$\forall$lcon]} here, we would be stuck. In the current system, we resolve the constraint to $\beta \sim a$.
 
-The rule {\sc [$\leq$l$\forall$var]} is also key in being able to type check the {\tt g = mempty} example above. Without it, we would rewrite $(\forall\, a.\, \textit{Monoid} \; a \Rightarrow a) \leq b$ to $\textit{Monoid} \; \alpha \wedge \alpha \leq b$. But this disallows progress, we want $\alpha \sim b$ instead.
-
-\item Note that these rules along with the generation and propagation ones ensure that no constraint of the form $\alpha \leq \sigma$, with $\alpha$ a unification variable, is ever produced.
+The rule {\sc [$\leq$lcon]} applied to type variables in the left-hand side is also key in being able to type check the {\tt g = mempty} example above. Without it, we would rewrite $(\forall\, a.\, \textit{Monoid} \; a \Rightarrow a) \leq b$ to $\textit{Monoid} \; \alpha \wedge \alpha \leq b$. But this disallows progress, we want $\alpha \sim b$ instead.
 \end{itemize}
 
 \subsubsection*{Design choice: rules for $\to$}
@@ -177,7 +180,7 @@ In the constraint solving process we do not only need to find a solution for the
 \paragraph{Rule {\sc [$\leq$refl]}.} We need to build $W :: \sigma \to \sigma$. This is easy:
 $$W = \lambda x. \; x$$
 
-\paragraph{Rule {\sc [$\leq$lcon]}.} We need to build $W_1 :: \psi_1 \to \sigma_2$. For this, we can use the evidence $W_2 :: \psi_1 \sim \sigma_2$ generated by later solving steps. In this case the solution is to make:
+\paragraph{Rule {\sc [$\leq$lcon]}.} We need to build $W_1 :: \sigma_1 \to \sigma_2$. For this, we can use the evidence $W_2 :: \sigma_1 \sim \sigma_2$ generated by later solving steps. In this case the solution is to make:
 $$W_1 = \lambda (x :: \sigma_1). \; x \rhd W_2$$
 where $\rhd$ is the cast operator which applies a coercion $\sigma_a \sim \sigma_b$ to a value of type $\sigma_a$ to produce the same value, but typed as $\sigma_b$.
 
@@ -186,9 +189,6 @@ $$\lambda (x :: \forall \overline{a}. Q_1 \Rightarrow \sigma_1). \; x \; \overli
 The last step is then applying $W_2$ to convert it to our desired type:
 $$W_1 = \lambda (x :: \forall \overline{a}. Q_1 \Rightarrow \sigma_1). \; W_2 \; (x \; \overline{\alpha} \; W_3)$$
 
-\paragraph{Rule {\sc [$\leq$l$\forall$var]}.} This case is similar to the previous one, but now $W_2 :: [\overline{a \mapsto \alpha}]v \sim \psi_2$. Instead of using application, we use a cast:
-$$W_1 = \lambda (x :: \forall \overline{a}. Q_1 \Rightarrow \sigma_1). \; (x \; \overline{\alpha} \; W_3) \rhd W_2$$
-
 \paragraph{Rule {\sc [$\leq$r$\forall$]}.} This is the most complicated rule for which to generate evidence. As usual, we want to generate evidence $W_1 :: \sigma_1 \to (\forall \overline{a}. Q_2 \Rightarrow \sigma_2)$. In order to do so, we can use the evidence generated by solving $\forall \overline{a}. \, (Q_2 \supset \sigma_1 \leq \sigma_2)$. In GHC, this implication generates two pieces of information: evidence $W_2 :: \sigma_1 \to \sigma_2$, and a series of bindings which might use the data in $Q_2$ and which make $W_2$ correct. We shall denote those bindings by $\square$.
 
 In this case, we need to generate something whose type is $\forall \overline{a}. Q_2 \Rightarrow \dots$. Thus, we need first a series of type abstractions and evidence abstractions. Then, we can just apply $W_2$ remembering to bring the bindings into scope.