[commit: ghc] wip/impredicativity: Add special rule for InstanceOf (forall a. a) (ad3678c)

Wed Jul 15 13:11:11 UTC 2015

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

On branch  : wip/impredicativity
Link       : http://ghc.haskell.org/trac/ghc/changeset/ad3678c73c3c395d9e306cd0a619814b6ae727d8/ghc

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

commit ad3678c73c3c395d9e306cd0a619814b6ae727d8
Author: Alejandro Serrano <trupill at gmail.com>
Date:   Wed Jul 15 15:09:43 2015 +0200

    Add special rule for InstanceOf (forall a. a)
    
    In several cases we obtain constraints of the form
    (forall a. a) <= something (for example,
    by using undefined). If we instantiate the variables,
    we get alpha <= something. If this something is
    again a variable, we are stuck.
    
    However, (forall a. a) <= something is always true.
    So, we add a new special rule for this case.


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

ad3678c73c3c395d9e306cd0a619814b6ae727d8
 compiler/typecheck/TcCanonical.hs | 30 +++++++++++++++++++++++++++---
 docs/types/impredicativity.ltx    | 18 ++++++++++++++++++
 2 files changed, 45 insertions(+), 3 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index d7932a8..8bc348f 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1660,11 +1660,16 @@ 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 InstanceOf (forall a. a) sigma -> nothing
+  | (vs, [], ty) <- tcSplitSigmaTy lhs
+  , Just v <- getTyVar_maybe ty
+  , v `elem` vs
+  = can_instance_null ev lhs rhs
     -- case InstanceOf (T ...) sigma --> T ... ~ sigma
   | is_not_forall lhs, Nothing <- getTyVar_maybe lhs
   = can_instance_to_eq ev lhs rhs
-  -- case InstanceOf (forall qvars. Q => ty) sigma
-  -- where sigma is T ..., F ... or a Skolem tyvar
+    -- case InstanceOf (forall qvars. Q => ty) sigma
+    -- where sigma is T ..., F ... or a Skolem tyvar
   | is_forall lhs
   , is_not_forall rhs               -- RHS is not a forall
   , Nothing <- getTyVar_maybe rhs   -- or a variabla
@@ -1681,7 +1686,7 @@ can_instance_of (CInstanceOfCan { cc_ev = ev, cc_lhs = lhs, cc_rhs = rhs })
            ; setWantedEvBind evar ev_let
            ; stopWith ev "can_instance_of/LET" }
       _ -> stopWith ev "Given/Derived instanceOf instantiation"
-  -- already canonical
+    -- already canonical
   | otherwise = continueWith (CIrredEvCan { cc_ev = ev })
   where
     is_not_forall ty
@@ -1722,3 +1727,22 @@ can_instance_inst ev lhs rhs
          ; traceTcS "can_instance_of/INST" (vcat [ ppr new_ev_ty, ppr new_ev_qs ])
          ; canInstanceOfNC new_ev_ty }
     _ -> stopWith ev "Given/Derived instanceOf instantiation"
+
+can_instance_null :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct)
+can_instance_null ev lhs rhs
+  = case ev of
+    CtWanted { ctev_evar = evar, ctev_loc = loc } ->
+      do { (qvars, _, ty) <- splitInst lhs
+           -- generate new constraints
+         ; let inst = mkInstanceOfPred ty rhs
+         ; new_ev_inst <- newWantedEvVarNC loc inst
+         ; let eq = mkTcEqPredRole Nominal ty rhs
+         ; new_ev_eq <- newWantedEvVarNC loc eq
+           -- set the evidence for the instantiation
+         ; let qvars' = map mkTyVarTy qvars
+         ; setWantedEvBind evar (mkInstanceOfInst lhs qvars' (ctEvId new_ev_inst) [])
+         ; setWantedEvBind (ctEvId new_ev_inst) (mkInstanceOfEq ty (ctEvCoercion new_ev_eq))
+           -- emit new work
+         ; traceTcS "can_instance_of/NULL" (vcat [ ppr new_ev_inst, ppr new_ev_eq ])
+         ; canEqNC new_ev_eq NomEq ty rhs }
+    _ -> stopWith ev "Given/Derived instanceOf instantiation"
diff --git a/docs/types/impredicativity.ltx b/docs/types/impredicativity.ltx
index 9234351..b62bd75 100644
--- a/docs/types/impredicativity.ltx
+++ b/docs/types/impredicativity.ltx
@@ -87,6 +87,7 @@ $$
 $$
 \begin{array}{lrcl}
 \textsc{[$\leq$refl]} & canon\left[\sigma \leq \sigma\right] & = & \sigma \sim \sigma \\
+\textsc{[$\leq$trivial]} & canon\left[(\forall a. a) \leq \sigma_2 \right] & = & \epsilon \\
 \textsc{[$\leq$lcon]} & canon\left[(\mathsf{D} \; \overline{\sigma_1}) \leq \sigma_2\right] & = & (\mathsf{D} \; \overline{\sigma_1}) \sim \sigma_2 \\
 \textsc{[$\leq$l$\forall$]} & canon\left[(\forall \overline{a}. Q_1 \Rightarrow \sigma_1) \leq \sigma_2\right] & = & [\overline{a \mapsto \alpha}]\sigma_1 \leq \sigma_2 \, \wedge \, [\overline{a \mapsto \alpha}]Q_1 \\
 & & & \textrm{where } \sigma_2 \textrm{ is } \mathsf{D} \; \overline{\sigma} \textrm{ or a Skolem variable} \\
@@ -94,6 +95,19 @@ $$
 \end{array}
 $$
 
+\subsubsection*{Notes on the {\sc [$\leq$trivial]} rule}
+
+Consider the following code, taken from the {\tt GHC.List} module:
+\begin{verbatim}
+head :: [a] -> a
+head (x:xs) = x
+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. However, it is the case that \emph{any} type is an instance of $\forall a. a$, so we have included an extra rule for this case. It seems very specific, but this scenario is quite common when calling functions such as {\tt error} or {\tt raise}.
+
 \subsubsection*{Notes on the {\sc [$\leq$l$\forall$]} rule}
 \begin{itemize}
 \item We disallow applying {\sc [$\leq$l$\forall$]} in the case of unification variables. 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.
@@ -127,6 +141,9 @@ In the constraint solving process we do not only need to find a solution for the
 $$W_1 = \lambda (x :: \sigma_1). \; x \rhd W_2$$
 where $\rhd$ is the cast operator which applies a coercion $\rho_1 \to \rho_2$ to a value of type $\rho_1$ to produce the same value, but typed as $\rho_2$.
 
+\paragraph{Rule {\sc [$\leq$trivial]}.} We need to build $W_1 :: (\forall a. a) \to \sigma_2$. This is simple type application:
+$$W_1 = \lambda (x :: \forall a. a). \; x \; \sigma_2$$
+
 \paragraph{Rule and {\sc [$\leq$l$\forall$]}.} We need to build $W_1 :: (\forall \overline{a}. Q_1 \Rightarrow \sigma_1) \to \sigma_2$ given $W_2 :: [\overline{a \mapsto \alpha}]\sigma_1 \to \sigma_2$ and $W_3 :: [\overline{a \mapsto \alpha}]Q_1$. The first step is to get $[\overline{a \mapsto \alpha}]\sigma_1$ from $\forall \overline{a}. Q_1 \Rightarrow \sigma_1$, to do that we need to make a type application and afterwards apply the witness for $Q_1 \Rightarrow \sigma_1$:
 $$\lambda (x :: \forall \overline{a}. Q_1 \Rightarrow \sigma_1). \; x \; \alpha \; W_3 :: (\forall \overline{a}. Q_1 \Rightarrow \sigma_1) \to [\overline{a \mapsto \alpha}]\sigma_1$$
 The last step is then applying $W_2$ to convert it to our desired type:
@@ -473,6 +490,7 @@ f x = S (error x)
 If we apply {\sc [AppFunNonVar]} directly, we instantiate the type of $error :: \forall b. [Char] \to b$ to $[Char] \to \beta$.
 Since we are pushing down a unification variable $\alpha$ because of the previous application of {\sc [AppFunNonVar]} to $S :: \forall a. \, a \to S \; a$, we obtain a constraint $\beta \leq \alpha$. Since there are no more restrictions to either $\alpha$ or $\beta$, we are not stuck in solving.
 
+\newpage
 \section*{Examples}
 \subsection*{\tt runST e}
 $$(\$)^{\alpha \to \beta \to \gamma} \; runST^\alpha \; \left( e \; :: \; \forall s. ST \; s \; Int \right)^\beta$$

