Substantial improvements to coercion optimisation
[ghc.git] / compiler / types / Unify.lhs
index 9137150..a9586b6 100644 (file)
@@ -16,7 +16,7 @@ module Unify (
        Refinement, emptyRefinement, isEmptyRefinement, 
        matchRefine, refineType, refinePred, refineResType,
 
-        -- side-effect free unification
+        -- Side-effect free unification
         tcUnifyTys, BindFlag(..)
 
    ) where
@@ -158,23 +158,19 @@ match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
                         | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
 
 match menv subst (TyVarTy tv1) ty2
+  | Just ty1' <- lookupVarEnv subst tv1'       -- tv1' is already bound
+  = if tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
+       -- ty1 has no locally-bound variables, hence nukeRnEnvL
+       -- Note tcEqType...we are doing source-type matching here
+    then Just subst
+    else Nothing       -- ty2 doesn't match
+
   | tv1' `elemVarSet` me_tmpls menv
-  = case lookupVarEnv subst tv1' of
-       Nothing         -- No existing binding
-           | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
-           -> Nothing  -- Occurs check
-           | otherwise 
-           -> do { subst1 <- match_kind menv subst tv1 ty2
-                 ; return (extendVarEnv subst1 tv1' ty2) }
+  = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
+    then Nothing       -- Occurs check
+    else do { subst1 <- match_kind menv subst tv1 ty2
                        -- Note [Matching kinds]
-
-       Just ty1'       -- There is an existing binding; check whether ty2 matches it
-           | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
-               -- ty1 has no locally-bound variables, hence nukeRnEnvL
-               -- Note tcEqType...we are doing source-type matching here
-           -> Just subst
-           | otherwise -> Nothing      -- ty2 doesn't match
-           
+           ; return (extendVarEnv subst1 tv1' ty2) }
 
    | otherwise -- tv1 is not a template tyvar
    = case ty2 of
@@ -210,7 +206,7 @@ match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
 -- Match the kind of the template tyvar with the kind of Type
 -- Note [Matching kinds]
 match_kind menv subst tv ty
-  | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
+  | isCoVar tv = do { let (ty1,ty2) = coVarKind tv
                          (ty3,ty4) = coercionKind ty
                    ; subst1 <- match menv subst ty1 ty3
                    ; match menv subst1 ty2 ty4 }
@@ -388,12 +384,12 @@ dataConCannotMatch tys con
 data Refinement = Reft InScopeSet InternalReft 
 
 type InternalReft = TyVarEnv (Coercion, Type)
--- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
+-- INVARIANT:   a->(co,ty)   then   co :: (a~ty)
 -- Not necessarily idemopotent
 
 instance Outputable Refinement where
   ppr (Reft _in_scope env)
-    = ptext SLIT("Refinement") <+>
+    = ptext (sLit "Refinement") <+>
         braces (ppr env)
 
 emptyRefinement :: Refinement
@@ -405,7 +401,7 @@ isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
 -- Apply the refinement to the type.
 -- If (refineType r ty) = (co, ty')
--- Then co :: ty:=:ty'
+-- Then co :: ty~ty'
 -- Nothing => the refinement does nothing to this type
 refineType (Reft in_scope env) ty
   | not (isEmptyVarEnv env),           -- Common case
@@ -431,7 +427,7 @@ refinePred (Reft in_scope env) pred
 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
 -- Like refineType, but returns the 'sym' coercion
 -- If (refineResType r ty) = (co, ty')
--- Then co :: ty':=:ty
+-- Then co :: ty'~ty
 refineResType reft ty
   = case refineType reft ty of
       Just (co, ty1) -> Just (mkSymCoercion co, ty1)
@@ -446,7 +442,7 @@ refineResType reft ty
 %************************************************************************
 
 \begin{code}
-matchRefine :: [CoVar] -> Refinement
+matchRefine :: [TyVar] -> [Coercion] -> Refinement
 \end{code}
 
 Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
@@ -466,19 +462,16 @@ Precondition: The rhs types must indeed be a specialisation of the lhs types;
 NB: matchRefine does *not* expand the type synonyms.
 
 \begin{code}
-matchRefine co_var
-  = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
+matchRefine in_scope_tvs co
+  = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
   where
-    in_scope = foldr extend emptyInScopeSet co_vars
+    in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
+       -- NB: in_scope_tvs include both coercion variables
+       --     *and* the tyvars in their kinds
 
-       -- For each co_var, add it *and* the tyvars it mentions, to in_scope
-    extend co_var in_scope
-      = extendInScopeSetSet in_scope $
-         extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
-
-    refineOne co_var = refine (TyVarTy co_var) ty1 ty2
+    refineOne co = refine co ty1 ty2
       where
-        (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
+        (ty1, ty2) = coercionKind co
 
     refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
     refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'
@@ -624,8 +617,8 @@ uVar :: TvSubstEnv  -- An existing substitution to extend
      -> UM TvSubstEnv
 
 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
---     if swap=False   (tv1:=:ty)
---     if swap=True    (ty:=:tv1)
+--     if swap=False   (tv1~ty)
+--     if swap=True    (ty~tv1)
 
 uVar subst tv1 ty
  = -- Check to see whether tv1 is refined by the substitution
@@ -647,7 +640,7 @@ uUnrefined subst tv1 ty2 ty2'
   = uUnrefined subst tv1 ty2 ty2''     -- Unwrap synonyms
                -- This is essential, in case we have
                --      type Foo a = a
-               -- and then unify a :=: Foo a
+               -- and then unify a ~ Foo a
 
 uUnrefined subst tv1 ty2 (TyVarTy tv2)
   | tv1 == tv2         -- Same type variable
@@ -663,15 +656,6 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2)
        ; b2 <- tvBindFlag tv2
        ; case (b1,b2) of
            (BindMe, _)          -> bind tv1 ty2
-
-           (AvoidMe, BindMe)    -> bind tv2 ty1
-           (AvoidMe, _)         -> bind tv1 ty2
-
-           (WildCard, WildCard) -> return subst
-           (WildCard, Skolem)   -> return subst
-           (WildCard, _)        -> bind tv2 ty1
-
-           (Skolem, WildCard)   -> return subst
            (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
            (Skolem, _)          -> bind tv2 ty1
        }
@@ -711,29 +695,33 @@ bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
 bindTv subst tv ty     -- ty is not a type variable
   = do  { b <- tvBindFlag tv
        ; case b of
-           Skolem   -> failWith (misMatch (TyVarTy tv) ty)
-           WildCard -> return subst
-           _other   -> return $ extendVarEnv subst tv ty
+           Skolem -> failWith (misMatch (TyVarTy tv) ty)
+           BindMe -> return $ extendVarEnv subst tv ty
        }
 \end{code}
 
 %************************************************************************
 %*                                                                     *
-               Unification monad
+               Binding decisions
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
 data BindFlag 
   = BindMe     -- A regular type variable
-  | AvoidMe    -- Like BindMe but, given the choice, avoid binding it
 
   | Skolem     -- This type variable is a skolem constant
                -- Don't bind it; it only matches itself
+\end{code}
 
-  | WildCard   -- This type variable matches anything,
-               -- and does not affect the substitution
 
+%************************************************************************
+%*                                                                     *
+               Unification monad
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
                         -> MaybeErr Message a }
 
@@ -771,23 +759,23 @@ maybeErrToMaybe (Failed _)    = Nothing
 \begin{code}
 misMatch :: Type -> Type -> SDoc
 misMatch t1 t2
-  = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+> 
-    ptext SLIT("and") <+> quotes (ppr t2)
+  = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+> 
+    ptext (sLit "and") <+> quotes (ppr t2)
 
 lengthMisMatch :: [Type] -> [Type] -> SDoc
 lengthMisMatch tys1 tys2
-  = sep [ptext SLIT("Can't match unequal length lists"), 
+  = sep [ptext (sLit "Can't match unequal length lists"), 
         nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 
 kindMisMatch :: TyVar -> Type -> SDoc
 kindMisMatch tv1 t2
-  = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
-           ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
-         ptext SLIT("when matching") <+> quotes (ppr tv1) <+> 
-               ptext SLIT("with") <+> quotes (ppr t2)]
+  = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
+           ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
+         ptext (sLit "when matching") <+> quotes (ppr tv1) <+> 
+               ptext (sLit "with") <+> quotes (ppr t2)]
 
 occursCheck :: TyVar -> Type -> SDoc
 occursCheck tv ty
-  = hang (ptext SLIT("Can't construct the infinite type"))
+  = hang (ptext (sLit "Can't construct the infinite type"))
        2 (ppr tv <+> equals <+> ppr ty)
 \end{code}