From a9895ec7414bc752df14a168600cfc7a2e50d3da Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Thu, 30 Apr 2020 15:32:57 +0100 Subject: Improve Note [The flattening story] --- compiler/GHC/Tc/Solver/Flatten.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/compiler/GHC/Tc/Solver/Flatten.hs b/compiler/GHC/Tc/Solver/Flatten.hs index 551e1de395..006e7865c0 100644 --- a/compiler/GHC/Tc/Solver/Flatten.hs +++ b/compiler/GHC/Tc/Solver/Flatten.hs @@ -41,7 +41,7 @@ import Control.Arrow ( first ) {- Note [The flattening story] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~~~~~~~~~~~~~~~ * A CFunEqCan is either of form [G] : F xis ~ fsk -- fsk is a FlatSkolTv [W] x : F xis ~ fmv -- fmv is a FlatMetaTv @@ -62,7 +62,8 @@ Note [The flattening story] - A unification flatten-skolem, fmv, stands for the as-yet-unknown type to which (F xis) will eventually reduce. It is filled in - + by dischargeFunEq, which calls unflattenFmv; this step will + happen during the interaction phase, after flattening. - All fsk/fmv variables are "untouchable". To make it simple to test, we simply give them TcLevel=0. This means that in a CTyVarEq, say, @@ -73,7 +74,7 @@ Note [The flattening story] a) The CFunEqCan takes a step, using an axiom b) By unflattenWanteds They are never unified in any other form of equality. - For example [W] ffmv ~ Int is stuck; it does not unify with fmv. + For example [W] fmv ~ Int is stuck; it does not unify with fmv. * We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan. That would destroy the invariant about the shape of a CFunEqCan, -- cgit v1.2.1