diff options
author | Austin Seipp <austin@well-typed.com> | 2014-09-25 23:07:07 -0500 |
---|---|---|
committer | Austin Seipp <austin@well-typed.com> | 2014-09-25 23:07:07 -0500 |
commit | efdf4b9d69d7eda83f872cbcfac9ef1215f39b7c (patch) | |
tree | 2378402156152b5cb56e5d91c6b6b5e57b1551a1 /compiler | |
parent | 18155ac21257316b430bfa209512d06822319707 (diff) | |
download | haskell-efdf4b9d69d7eda83f872cbcfac9ef1215f39b7c.tar.gz |
types: detabify/dewhitespace Unify
Signed-off-by: Austin Seipp <austin@well-typed.com>
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/types/Unify.lhs | 351 |
1 files changed, 172 insertions, 179 deletions
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 709c0e5ecc..fe81d06e05 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -4,23 +4,17 @@ \begin{code} {-# LANGUAGE CPP #-} -{-# OPTIONS_GHC -fno-warn-tabs #-} --- The above warning supression flag is a temporary kludge. --- While working on this module you are encouraged to remove it and --- detab the module (please do the detabbing in a separate patch). See --- http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces --- for details -module Unify ( - -- Matching of types: - -- the "tc" prefix indicates that matching always - -- respects newtypes (rather than looking through them) - tcMatchTy, tcMatchTys, tcMatchTyX, - ruleMatchTyX, tcMatchPreds, +module Unify ( + -- Matching of types: + -- the "tc" prefix indicates that matching always + -- respects newtypes (rather than looking through them) + tcMatchTy, tcMatchTys, tcMatchTyX, + ruleMatchTyX, tcMatchPreds, - MatchEnv(..), matchList, + MatchEnv(..), matchList, - typesCantMatch, + typesCantMatch, -- Side-effect free unification tcUnifyTy, tcUnifyTys, BindFlag(..), @@ -48,9 +42,9 @@ import Control.Applicative (Applicative(..)) %************************************************************************ -%* * - Matching -%* * +%* * + Matching +%* * %************************************************************************ @@ -59,8 +53,8 @@ Matching is much tricker than you might think. 1. The substitution we generate binds the *template type variables* which are given to us explicitly. -2. We want to match in the presence of foralls; - e.g (forall a. t1) ~ (forall b. t2) +2. We want to match in the presence of foralls; + e.g (forall a. t1) ~ (forall b. t2) That is what the RnEnv2 is for; it does the alpha-renaming that makes it as if a and b were the same variable. @@ -70,7 +64,7 @@ Matching is much tricker than you might think. 3. We must be careful not to bind a template type variable to a locally bound variable. E.g. - (forall a. x) ~ (forall b. b) + (forall a. x) ~ (forall b. b) 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. @@ -78,61 +72,61 @@ Matching is much tricker than you might think. \begin{code} data MatchEnv - = ME { me_tmpls :: VarSet -- Template variables - , me_env :: RnEnv2 -- Renaming envt for nested foralls - } -- In-scope set includes template variables + = ME { me_tmpls :: VarSet -- Template variables + , me_env :: RnEnv2 -- Renaming envt for nested foralls + } -- In-scope set includes template variables -- Nota Bene: MatchEnv isn't specific to Types. It is used -- for matching terms and coercions as well as types -tcMatchTy :: TyVarSet -- Template tyvars - -> Type -- Template - -> Type -- Target - -> Maybe TvSubst -- One-shot; in principle the template - -- variables could be free in the target +tcMatchTy :: TyVarSet -- Template tyvars + -> Type -- Template + -> Type -- Target + -> Maybe TvSubst -- One-shot; in principle the template + -- variables could be free in the target tcMatchTy tmpls ty1 ty2 = case match menv emptyTvSubstEnv ty1 ty2 of - Just subst_env -> Just (TvSubst in_scope subst_env) - Nothing -> Nothing + Just subst_env -> Just (TvSubst in_scope subst_env) + Nothing -> Nothing where menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope } in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2) - -- We're assuming that all the interesting - -- tyvars in tys1 are in tmpls + -- We're assuming that all the interesting + -- tyvars in tys1 are in tmpls -tcMatchTys :: TyVarSet -- Template tyvars - -> [Type] -- Template - -> [Type] -- Target - -> Maybe TvSubst -- One-shot; in principle the template - -- variables could be free in the target +tcMatchTys :: TyVarSet -- Template tyvars + -> [Type] -- Template + -> [Type] -- Target + -> Maybe TvSubst -- One-shot; in principle the template + -- variables could be free in the target tcMatchTys tmpls tys1 tys2 = case match_tys menv emptyTvSubstEnv tys1 tys2 of - Just subst_env -> Just (TvSubst in_scope subst_env) - Nothing -> Nothing + Just subst_env -> Just (TvSubst in_scope subst_env) + Nothing -> Nothing where menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope } in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2) - -- We're assuming that all the interesting - -- tyvars in tys1 are in tmpls + -- We're assuming that all the interesting + -- tyvars in tys1 are in tmpls -- This is similar, but extends a substitution -tcMatchTyX :: TyVarSet -- Template tyvars - -> TvSubst -- Substitution to extend - -> Type -- Template - -> Type -- Target - -> Maybe TvSubst +tcMatchTyX :: TyVarSet -- Template tyvars + -> TvSubst -- Substitution to extend + -> Type -- Template + -> Type -- Target + -> Maybe TvSubst tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2 = case match menv subst_env ty1 ty2 of - Just subst_env -> Just (TvSubst in_scope subst_env) - Nothing -> Nothing + Just subst_env -> Just (TvSubst in_scope subst_env) + Nothing -> Nothing where menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope} tcMatchPreds - :: [TyVar] -- Bind these - -> [PredType] -> [PredType] - -> Maybe TvSubstEnv + :: [TyVar] -- Bind these + -> [PredType] -> [PredType] + -> Maybe TvSubstEnv tcMatchPreds tmpls ps1 ps2 = matchList (match menv) emptyTvSubstEnv ps1 ps2 where @@ -140,65 +134,65 @@ tcMatchPreds tmpls ps1 ps2 in_scope_tyvars = mkInScopeSet (tyVarsOfTypes ps1 `unionVarSet` tyVarsOfTypes ps2) -- This one is called from the expression matcher, which already has a MatchEnv in hand -ruleMatchTyX :: MatchEnv - -> TvSubstEnv -- Substitution to extend - -> Type -- Template - -> Type -- Target - -> Maybe TvSubstEnv +ruleMatchTyX :: MatchEnv + -> TvSubstEnv -- Substitution to extend + -> Type -- Template + -> Type -- Target + -> Maybe TvSubstEnv -ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export +ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export \end{code} Now the internals of matching \begin{code} -match :: MatchEnv -- For the most part this is pushed downwards - -> TvSubstEnv -- Substitution so far: - -- Domain is subset of template tyvars - -- Free vars of range is subset of - -- in-scope set of the RnEnv2 - -> Type -> Type -- Template and target respectively +match :: MatchEnv -- For the most part this is pushed downwards + -> TvSubstEnv -- Substitution so far: + -- Domain is subset of template tyvars + -- Free vars of range is subset of + -- in-scope set of the RnEnv2 + -> Type -> Type -- Template and target respectively -> Maybe TvSubstEnv match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2 - | Just ty2' <- coreView ty2 = 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 + | Just ty1' <- lookupVarEnv subst tv1' -- tv1' is already bound = if eqTypeX (nukeRnEnvL rn_env) ty1' ty2 - -- ty1 has no locally-bound variables, hence nukeRnEnvL + -- ty1 has no locally-bound variables, hence nukeRnEnvL then Just subst - else Nothing -- ty2 doesn't match + else Nothing -- ty2 doesn't match | tv1' `elemVarSet` me_tmpls menv = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2)) - then Nothing -- Occurs check + then Nothing -- Occurs check else do { subst1 <- match_kind menv subst (tyVarKind tv1) (typeKind ty2) - -- Note [Matching kinds] - ; return (extendVarEnv subst1 tv1' ty2) } + -- Note [Matching kinds] + ; return (extendVarEnv subst1 tv1' ty2) } - | otherwise -- tv1 is not a template tyvar + | otherwise -- tv1 is not a template tyvar = case ty2 of - TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst - _ -> Nothing + TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst + _ -> Nothing where rn_env = me_env menv tv1' = rnOccL rn_env tv1 -match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) +match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) = do { subst' <- match_kind menv subst (tyVarKind tv1) (tyVarKind tv2) ; match menv' subst' ty1 ty2 } - where -- Use the magic of rnBndr2 to go under the binders + where -- Use the magic of rnBndr2 to go under the binders menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 } -match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) +match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2 = match_tys menv subst tys1 tys2 -match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) +match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) = do { subst' <- match menv subst ty1a ty2a ; match menv subst' ty1b ty2b } match menv subst (AppTy ty1a ty1b) ty2 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2 - -- 'repSplit' used because the tcView stuff is done above + -- 'repSplit' used because the tcView stuff is done above = do { subst' <- match menv subst ty1a ty2a ; match menv subst' ty1b ty2b } @@ -222,13 +216,13 @@ match_kind menv subst k1 k2 -- Note [Matching kinds] -- ~~~~~~~~~~~~~~~~~~~~~ --- For ordinary type variables, we don't want (m a) to match (n b) --- if say (a::*) and (b::*->*). This is just a yes/no issue. +-- For ordinary type variables, we don't want (m a) to match (n b) +-- if say (a::*) and (b::*->*). This is just a yes/no issue. -- --- For coercion kinds matters are more complicated. If we have a +-- For coercion kinds matters are more complicated. If we have a -- coercion template variable co::a~[b], where a,b are presumably also --- template type variables, then we must match co's kind against the --- kind of the actual argument, so as to give bindings to a,b. +-- template type variables, then we must match co's kind against the +-- kind of the actual argument, so as to give bindings to a,b. -- -- In fact I have no example in mind that *requires* this kind-matching -- to instantiate template type variables, but it seems like the right @@ -240,51 +234,51 @@ match_tys menv subst tys1 tys2 = matchList (match menv) subst tys1 tys2 -------------- matchList :: (env -> a -> b -> Maybe env) - -> env -> [a] -> [b] -> Maybe env + -> env -> [a] -> [b] -> Maybe env matchList _ subst [] [] = Just subst matchList fn subst (a:as) (b:bs) = do { subst' <- fn subst a b - ; matchList fn subst' as bs } + ; matchList fn subst' as bs } matchList _ _ _ _ = Nothing \end{code} %************************************************************************ -%* * - GADTs -%* * +%* * + GADTs +%* * %************************************************************************ Note [Pruning dead case alternatives] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider data T a where - T1 :: T Int - T2 :: T a +Consider data T a where + T1 :: T Int + T2 :: T a - newtype X = MkX Int - newtype Y = MkY Char + newtype X = MkX Int + newtype Y = MkY Char - type family F a - type instance F Bool = Int + type family F a + type instance F Bool = Int -Now consider case x of { T1 -> e1; T2 -> e2 } +Now consider case x of { T1 -> e1; T2 -> e2 } The question before the house is this: if I know something about the type of x, can I prune away the T1 alternative? -Suppose x::T Char. It's impossible to construct a (T Char) using T1, - Answer = YES we can prune the T1 branch (clearly) +Suppose x::T Char. It's impossible to construct a (T Char) using T1, + Answer = YES we can prune the T1 branch (clearly) Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated to 'Bool', in which case x::T Int, so - ANSWER = NO (clearly) + ANSWER = NO (clearly) -Suppose x::T X. Then *in Haskell* it's impossible to construct a (non-bottom) +Suppose x::T X. Then *in Haskell* it's impossible to construct a (non-bottom) value of type (T X) using T1. But *in FC* it's quite possible. The newtype gives a coercion - CoX :: X ~ Int + CoX :: X ~ Int So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value of type (T X) constructed with T1. Hence - ANSWER = NO we can't prune the T1 branch (surprisingly) + ANSWER = NO we can't prune the T1 branch (surprisingly) Furthermore, this can even happen; see Trac #1251. GHC's newtype-deriving mechanism uses a cast, just as above, to move from one dictionary to another, @@ -295,21 +289,21 @@ non-bottom value of type (T Y) using T1. That's because we can get from Y to Char, but not to Int. -Here's a related question. data Eq a b where EQ :: Eq a a +Here's a related question. data Eq a b where EQ :: Eq a a Consider - case x of { EQ -> ... } + case x of { EQ -> ... } Suppose x::Eq Int Char. Is the alternative dead? Clearly yes. What about x::Eq Int a, in a context where we have evidence that a~Char. -Then again the alternative is dead. +Then again the alternative is dead. - Summary + Summary We are really doing a test for unsatisfiability of the type constraints implied by the match. And that is clearly, in general, a -hard thing to do. +hard thing to do. However, since we are simply dropping dead code, a conservative test suffices. There is a continuum of tests, ranging from easy to hard, that @@ -325,40 +319,40 @@ typesCantMatch prs = any (\(s,t) -> cant_match s t) prs where cant_match :: Type -> Type -> Bool cant_match t1 t2 - | Just t1' <- coreView t1 = cant_match t1' t2 - | Just t2' <- coreView t2 = cant_match t1 t2' + | Just t1' <- coreView t1 = cant_match t1' t2 + | Just t2' <- coreView t2 = cant_match t1 t2' cant_match (FunTy a1 r1) (FunTy a2 r2) - = cant_match a1 a2 || cant_match r1 r2 + = cant_match a1 a2 || cant_match r1 r2 cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2) - | isDistinctTyCon tc1 && isDistinctTyCon tc2 - = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2) + | isDistinctTyCon tc1 && isDistinctTyCon tc2 + = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2) cant_match (FunTy {}) (TyConApp tc _) = isDistinctTyCon tc cant_match (TyConApp tc _) (FunTy {}) = isDistinctTyCon tc - -- tc can't be FunTyCon by invariant + -- tc can't be FunTyCon by invariant cant_match (AppTy f1 a1) ty2 - | Just (f2, a2) <- repSplitAppTy_maybe ty2 - = cant_match f1 f2 || cant_match a1 a2 + | Just (f2, a2) <- repSplitAppTy_maybe ty2 + = cant_match f1 f2 || cant_match a1 a2 cant_match ty1 (AppTy f2 a2) - | Just (f1, a1) <- repSplitAppTy_maybe ty1 - = cant_match f1 f2 || cant_match a1 a2 + | Just (f1, a1) <- repSplitAppTy_maybe ty1 + = cant_match f1 f2 || cant_match a1 a2 cant_match (LitTy x) (LitTy y) = x /= y cant_match _ _ = False -- Safe! -- Things we could add; --- foralls --- look through newtypes --- take account of tyvar bindings (EQ example above) +-- foralls +-- look through newtypes +-- take account of tyvar bindings (EQ example above) \end{code} %************************************************************************ -%* * +%* * Unification %* * %************************************************************************ @@ -442,7 +436,7 @@ usages won't notice this design choice. \begin{code} tcUnifyTy :: Type -> Type -- All tyvars are bindable - -> Maybe TvSubst -- A regular one-shot (idempotent) substitution + -> Maybe TvSubst -- A regular one-shot (idempotent) substitution -- Simple unification of two types; all type variables are bindable tcUnifyTy ty1 ty2 = case initUM (const BindMe) (unify emptyTvSubstEnv ty1 ty2) of @@ -451,8 +445,8 @@ tcUnifyTy ty1 ty2 ----------------- tcUnifyTys :: (TyVar -> BindFlag) - -> [Type] -> [Type] - -> Maybe TvSubst -- A regular one-shot (idempotent) substitution + -> [Type] -> [Type] + -> Maybe TvSubst -- A regular one-shot (idempotent) substitution -- The two types may have common type variables, and indeed do so in the -- second call to tcUnifyTys in FunDeps.checkClsFD tcUnifyTys bind_fn tys1 tys2 @@ -477,15 +471,15 @@ tcUnifyTysFG bind_fn tys1 tys2 = initUM bind_fn $ do { subst <- unifyList emptyTvSubstEnv tys1 tys2 - -- Find the fixed point of the resulting non-idempotent substitution + -- Find the fixed point of the resulting non-idempotent substitution ; return (niFixTvSubst subst) } \end{code} %************************************************************************ -%* * +%* * Non-idempotent substitution -%* * +%* * %************************************************************************ Note [Non-idempotent substitution] @@ -532,7 +526,7 @@ niFixTvSubst env = f env all_range_tvs = closeOverKinds range_tvs subst = mkTvSubst (mkInScopeSet all_range_tvs) env - -- env' extends env by replacing any free type with + -- env' extends env by replacing any free type with -- that same tyvar with a substituted kind -- See note [Finding the substitution fixpoint] env' = extendVarEnvList env [ (rtv, mkTyVarTy $ setTyVarKind rtv $ @@ -549,21 +543,21 @@ niSubstTvSet subst tvs = foldVarSet (unionVarSet . get) emptyVarSet tvs where get tv = case lookupVarEnv subst tv of - Nothing -> unitVarSet tv + Nothing -> unitVarSet tv Just ty -> niSubstTvSet subst (tyVarsOfType ty) \end{code} %************************************************************************ -%* * - The workhorse -%* * +%* * + The workhorse +%* * %************************************************************************ \begin{code} -unify :: TvSubstEnv -- An existing substitution to extend - -> Type -> Type -- Types to be unified, and witness of their equality - -> UM TvSubstEnv -- Just the extended substitution, - -- Nothing if unification failed +unify :: TvSubstEnv -- An existing substitution to extend + -> Type -> Type -- Types to be unified, and witness of their equality + -> UM TvSubstEnv -- Just the extended substitution, + -- Nothing if unification failed -- We do not require the incoming substitution to be idempotent, -- nor guarantee that the outgoing one is. That's fixed up by -- the wrappers. @@ -577,32 +571,32 @@ unify subst ty1 (TyVarTy tv2) = uVar subst tv2 ty1 unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2 unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2' -unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) - | tyc1 == tyc2 +unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) + | tyc1 == tyc2 = unify_tys subst tys1 tys2 -unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) - = do { subst' <- unify subst ty1a ty2a - ; unify subst' ty1b ty2b } +unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) + = do { subst' <- unify subst ty1a ty2a + ; unify subst' ty1b ty2b } - -- Applications need a bit of care! - -- They can match FunTy and TyConApp, so use splitAppTy_maybe - -- NB: we've already dealt with type variables and Notes, - -- so if one type is an App the other one jolly well better be too + -- Applications need a bit of care! + -- They can match FunTy and TyConApp, so use splitAppTy_maybe + -- NB: we've already dealt with type variables and Notes, + -- so if one type is an App the other one jolly well better be too unify subst (AppTy ty1a ty1b) ty2 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2 - = do { subst' <- unify subst ty1a ty2a + = do { subst' <- unify subst ty1a ty2a ; unify subst' ty1b ty2b } unify subst ty1 (AppTy ty2a ty2b) | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1 - = do { subst' <- unify subst ty1a ty2a + = do { subst' <- unify subst ty1a ty2a ; unify subst' ty1b ty2b } unify subst (LitTy x) (LitTy y) | x == y = return subst unify _ _ _ = surelyApart - -- ForAlls?? + -- ForAlls?? ------------------------------ unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv @@ -614,11 +608,11 @@ unifyList subst orig_xs orig_ys where go subst [] [] = return subst go subst (x:xs) (y:ys) = do { subst' <- unify subst x y - ; go subst' xs ys } + ; go subst' xs ys } go subst _ _ = maybeApart subst -- See Note [Lists of different lengths are MaybeApart] --------------------------------- -uVar :: TvSubstEnv -- An existing substitution to extend +uVar :: TvSubstEnv -- An existing substitution to extend -> TyVar -- Type variable to be unified -> Type -- with this type -> UM TvSubstEnv @@ -628,7 +622,7 @@ uVar subst tv1 ty case (lookupVarEnv subst tv1) of Just ty' -> unify subst ty' ty -- Yes, call back into unify' Nothing -> uUnrefined subst -- No, continue - tv1 ty ty + tv1 ty ty uUnrefined :: TvSubstEnv -- An existing substitution to extend -> TyVar -- Type variable to be unified @@ -640,13 +634,13 @@ uUnrefined :: TvSubstEnv -- An existing substitution to extend uUnrefined subst tv1 ty2 ty2' | Just ty2'' <- tcView 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 + = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms + -- This is essential, in case we have + -- type Foo a = a + -- and then unify a ~ Foo a uUnrefined subst tv1 ty2 (TyVarTy tv2) - | tv1 == tv2 -- Same type variable + | tv1 == tv2 -- Same type variable = return subst -- Check to see whether tv2 is refined @@ -658,10 +652,10 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2) = do { -- So both are unrefined; unify the kinds ; subst' <- unify subst (tyVarKind tv1) (tyVarKind tv2) - -- And then bind one or the other, + -- And then bind one or the other, -- depending on which is bindable - -- NB: unlike TcUnify we do not have an elaborate sub-kinding - -- story. That is relevant only during type inference, and + -- NB: unlike TcUnify we do not have an elaborate sub-kinding + -- story. That is relevant only during type inference, and -- (I very much hope) is not relevant here. ; b1 <- tvBindFlag tv1 ; b2 <- tvBindFlag tv2 @@ -671,51 +665,51 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2) (BindMe, _) -> return (extendVarEnv subst' tv1 ty2) (_, BindMe) -> return (extendVarEnv subst' tv2 ty1) } -uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable +uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2') = maybeApart subst -- Occurs check -- See Note [Fine-grained unification] | otherwise = do { subst' <- unify subst k1 k2 -- Note [Kinds Containing Only Literals] - ; bindTv subst' tv1 ty2 } -- Bind tyvar to the synonym if poss + ; bindTv subst' tv1 ty2 } -- Bind tyvar to the synonym if poss where k1 = tyVarKind tv1 k2 = typeKind ty2' bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv -bindTv subst tv ty -- ty is not a type variable +bindTv subst tv ty -- ty is not a type variable = do { b <- tvBindFlag tv - ; case b of - Skolem -> maybeApart subst -- See Note [Unification with skolems] - BindMe -> return $ extendVarEnv subst tv ty - } + ; case b of + Skolem -> maybeApart subst -- See Note [Unification with skolems] + BindMe -> return $ extendVarEnv subst tv ty + } \end{code} %************************************************************************ -%* * - Binding decisions -%* * +%* * + Binding decisions +%* * %************************************************************************ \begin{code} -data BindFlag - = BindMe -- A regular type variable +data BindFlag + = BindMe -- A regular type variable - | Skolem -- This type variable is a skolem constant - -- Don't bind it; it only matches itself + | Skolem -- This type variable is a skolem constant + -- Don't bind it; it only matches itself \end{code} %************************************************************************ -%* * - Unification monad -%* * +%* * + Unification monad +%* * %************************************************************************ \begin{code} newtype UM a = UM { unUM :: (TyVar -> BindFlag) - -> UnifyResultM a } + -> UnifyResultM a } instance Functor UM where fmap = liftM @@ -728,7 +722,7 @@ instance Monad UM where return a = UM (\_tvs -> Unifiable a) fail _ = UM (\_tvs -> SurelyApart) -- failed pattern match m >>= k = UM (\tvs -> case unUM m tvs of - Unifiable v -> unUM (k v) tvs + Unifiable v -> unUM (k v) tvs MaybeApart v -> case unUM (k v) tvs of Unifiable v' -> MaybeApart v' @@ -747,4 +741,3 @@ maybeApart subst = UM (\_tv_fn -> MaybeApart subst) surelyApart :: UM a surelyApart = UM (\_tv_fn -> SurelyApart) \end{code} - |