[commit: ghc] master: Comments in Unify, fixing #12442 (3483423)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/34834234fff4a9dd0408d3b29e001cd132665327/ghc

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

commit 34834234fff4a9dd0408d3b29e001cd132665327
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Thu Feb 22 10:44:18 2018 -0500

    Comments in Unify, fixing #12442
    
    [ci skip]


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

34834234fff4a9dd0408d3b29e001cd132665327
 compiler/types/Unify.hs | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index b401e1b..2c9762c 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -70,6 +70,34 @@ Unification is much tricker than you might think.
    where x is the template type variable.  Then we do not want to
    bind x to a/b!  This is a kind of occurs check.
    The necessary locals accumulate in the RnEnv2.
+
+Note [tcMatchTy vs tcMatchTyKi]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This module offers two variants of matching: with kinds and without.
+The TyKi variant takes two types, of potentially different kinds,
+and matches them. Along the way, it necessarily also matches their
+kinds. The Ty variant instead assumes that the kinds are already
+eqType and so skips matching up the kinds.
+
+How do you choose between them?
+
+1. If you know that the kinds of the two types are eqType, use
+   the Ty variant. It is more efficient, as it does less work.
+
+2. If the kinds of variables in the  template type might mention type families,
+   use the Ty variant (and do other work to make sure the kinds
+   work out). These pure unification functions do a straightforward
+   syntactic unification and do no complex reasoning about type
+   families. Note that the types of the variables in instances can indeed
+   mention type families, so instance lookup must use the Ty variant.
+
+   (Nothing goes terribly wrong -- no panics -- if there might be type
+   families in kinds in the TyKi variant. You just might get match
+   failure even though a reducing a type family would lead to success.)
+
+3. Otherwise, if you're sure that the variable kinds to not mention
+   type families and you're not already sure that the kind of the template
+   equals the kind of the target, then use the TyKi versio.n
 -}
 
 -- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
@@ -83,15 +111,18 @@ Unification is much tricker than you might think.
 -- by the match, because tcMatchTy (and similar functions) are
 -- always used on top-level types, so we can bind any of the
 -- free variables of the LHS.
+-- See also Note [tcMatchTy vs tcMatchTyKi]
 tcMatchTy :: Type -> Type -> Maybe TCvSubst
 tcMatchTy ty1 ty2 = tcMatchTys [ty1] [ty2]
 
 -- | Like 'tcMatchTy', but allows the kinds of the types to differ,
 -- and thus matches them as well.
+-- See also Note [tcMatchTy vs tcMatchTyKi]
 tcMatchTyKi :: Type -> Type -> Maybe TCvSubst
 tcMatchTyKi ty1 ty2 = tcMatchTyKis [ty1] [ty2]
 
 -- | This is similar to 'tcMatchTy', but extends a substitution
+-- See also Note [tcMatchTy vs tcMatchTyKi]
 tcMatchTyX :: TCvSubst            -- ^ Substitution to extend
            -> Type                -- ^ Template
            -> Type                -- ^ Target
@@ -99,6 +130,7 @@ tcMatchTyX :: TCvSubst            -- ^ Substitution to extend
 tcMatchTyX subst ty1 ty2 = tcMatchTysX subst [ty1] [ty2]
 
 -- | Like 'tcMatchTy' but over a list of types.
+-- See also Note [tcMatchTy vs tcMatchTyKi]
 tcMatchTys :: [Type]         -- ^ Template
            -> [Type]         -- ^ Target
            -> Maybe TCvSubst -- ^ One-shot; in principle the template
@@ -109,6 +141,7 @@ tcMatchTys tys1 tys2
     in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
 
 -- | Like 'tcMatchTyKi' but over a list of types.
+-- See also Note [tcMatchTy vs tcMatchTyKi]
 tcMatchTyKis :: [Type]         -- ^ Template
              -> [Type]         -- ^ Target
              -> Maybe TCvSubst -- ^ One-shot substitution
@@ -118,6 +151,7 @@ tcMatchTyKis tys1 tys2
     in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
 
 -- | Like 'tcMatchTys', but extending a substitution
+-- See also Note [tcMatchTy vs tcMatchTyKi]
 tcMatchTysX :: TCvSubst       -- ^ Substitution to extend
             -> [Type]         -- ^ Template
             -> [Type]         -- ^ Target
@@ -126,6 +160,7 @@ tcMatchTysX subst tys1 tys2
   = tc_match_tys_x False subst tys1 tys2
 
 -- | Like 'tcMatchTyKis', but extending a substitution
+-- See also Note [tcMatchTy vs tcMatchTyKi]
 tcMatchTyKisX :: TCvSubst        -- ^ Substitution to extend
               -> [Type]          -- ^ Template
               -> [Type]          -- ^ Target
@@ -463,6 +498,17 @@ tc_unify_tys :: (TyVar -> BindFlag)
              -> CvSubstEnv
              -> [Type] -> [Type]
              -> UnifyResultM (TvSubstEnv, CvSubstEnv)
+-- NB: It's tempting to ASSERT here that, if we're not matching kinds, then
+-- the kinds of the types should be the same. However, this doesn't work,
+-- as the types may be a dependent telescope, where later types have kinds
+-- that mention variables occuring earlier in the list of types. Here's an
+-- example (from typecheck/should_fail/T12709):
+--   template: [rep :: RuntimeRep,       a :: TYPE rep]
+--   target:   [LiftedRep :: RuntimeRep, Int :: TYPE LiftedRep]
+-- We can see that matching the first pair will make the kinds of the second
+-- pair equal. Yet, we still don't need a separate pass to unify the kinds
+-- of these types, so it's appropriate to use the Ty variant of unification.
+-- See also Note [tcMatchTy vs tcMatchTyKi].
 tc_unify_tys bind_fn unif inj_check match_kis rn_env tv_env cv_env tys1 tys2
   = initUM tv_env cv_env $
     do { when match_kis $