types: detabify/dewhitespace Unify
authorAustin Seipp <austin@well-typed.com>
Fri, 26 Sep 2014 04:07:07 +0000 (23:07 -0500)
committerAustin Seipp <austin@well-typed.com>
Fri, 26 Sep 2014 04:07:07 +0000 (23:07 -0500)
Signed-off-by: Austin Seipp <austin@well-typed.com>
compiler/types/Unify.lhs

index 709c0e5..fe81d06 100644 (file)
@@ -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}
-