Fix the pure unifier
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 16 May 2017 14:43:55 +0000 (15:43 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 16 May 2017 14:46:33 +0000 (15:46 +0100)
This patch fixes Trac #13705, by fixing a long-standing outright bug
in the pure unifier.  I'm surprised this hasn't caused more trouble
before now!

compiler/types/Unify.hs
testsuite/tests/indexed-types/should_compile/T13705.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T

index 6dc5f01..79d0897 100644 (file)
@@ -455,7 +455,7 @@ tc_unify_tys_fg match_kis bind_fn tys1 tys2
 -- | This function is actually the one to call the unifier -- a little
 -- too general for outside clients, though.
 tc_unify_tys :: (TyVar -> BindFlag)
-             -> Bool        -- ^ True <=> unify; False <=> match
+             -> AmIUnifying -- ^ True <=> unify; False <=> match
              -> Bool        -- ^ True <=> doing an injectivity check
              -> Bool        -- ^ True <=> treat the kinds as well
              -> RnEnv2
@@ -464,12 +464,17 @@ tc_unify_tys :: (TyVar -> BindFlag)
              -> [Type] -> [Type]
              -> UnifyResultM (TvSubstEnv, CvSubstEnv)
 tc_unify_tys bind_fn unif inj_check match_kis rn_env tv_env cv_env tys1 tys2
-  = initUM bind_fn unif inj_check rn_env tv_env cv_env $
+  = initUM tv_env cv_env $
     do { when match_kis $
-         unify_tys kis1 kis2
-       ; unify_tys tys1 tys2
+         unify_tys env kis1 kis2
+       ; unify_tys env tys1 tys2
        ; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
   where
+    env = UMEnv { um_bind_fun = bind_fn
+                , um_unif     = unif
+                , um_inj_tf   = inj_check
+                , um_rn_env   = rn_env }
+
     kis1 = map typeKind tys1
     kis2 = map typeKind tys2
 
@@ -664,7 +669,7 @@ this, but we musn't map a to anything else!)
 We thus must parameterize the algorithm over whether it's being used
 for an injectivity check (refrain from looking at non-injective arguments
 to type families) or not (do indeed look at those arguments).  This is
-implemented  by the uf_int_tf field of UmEnv.
+implemented  by the uf_inj_tf field of UmEnv.
 
 (It's all a question of whether or not to include equation (7) from Fig. 2
 of [ITF].)
@@ -770,151 +775,158 @@ coercions in this manner.
 
 -------------- unify_ty: the main workhorse -----------
 
-unify_ty :: Type -> Type  -- Types to be unified and a co
+type AmIUnifying = Bool   -- True  <=> Unifying
+                          -- False <=> Matching
+
+unify_ty :: UMEnv
+         -> Type -> Type  -- Types to be unified and a co
          -> Coercion      -- A coercion between their kinds
                           -- See Note [Kind coercions in Unify]
          -> UM ()
 -- See Note [Specification of unification]
 -- Respects newtypes, PredTypes
 
-unify_ty ty1 ty2 kco
+unify_ty env ty1 ty2 kco
     -- TODO: More commentary needed here
-  | Just ty1' <- tcView ty1   = unify_ty ty1' ty2 kco
-  | Just ty2' <- tcView ty2   = unify_ty ty1 ty2' kco
-  | CastTy ty1' co <- ty1     = unify_ty ty1' ty2 (co `mkTransCo` kco)
-  | CastTy ty2' co <- ty2     = unify_ty ty1 ty2' (kco `mkTransCo` mkSymCo co)
-
-unify_ty (TyVarTy tv1) ty2 kco = uVar tv1 ty2 kco
-unify_ty ty1 (TyVarTy tv2) kco
-  = do { unif <- amIUnifying
-       ; if unif
-         then umSwapRn $ uVar tv2 ty1 (mkSymCo kco)
-         else surelyApart }  -- non-tv on left; tv on right: can't match.
-
-unify_ty ty1 ty2 _kco
-  | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
-  , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
-  = if tc1 == tc2 || (tcIsStarKind ty1 && tcIsStarKind ty2)
-    then if isInjectiveTyCon tc1 Nominal
-         then unify_tys tys1 tys2
-         else do { let inj | isTypeFamilyTyCon tc1
-                           = case familyTyConInjectivityInfo tc1 of
+  | Just ty1' <- tcView ty1   = unify_ty env ty1' ty2 kco
+  | Just ty2' <- tcView ty2   = unify_ty env ty1 ty2' kco
+  | CastTy ty1' co <- ty1     = unify_ty env ty1' ty2 (co `mkTransCo` kco)
+  | CastTy ty2' co <- ty2     = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co)
+
+unify_ty env (TyVarTy tv1) ty2 kco
+  = uVar env tv1 ty2 kco
+unify_ty env ty1 (TyVarTy tv2) kco
+  | um_unif env  -- If unifying, can swap args
+  = uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
+
+unify_ty env ty1 ty2 _kco
+  | Just (tc1, tys1) <- mb_tc_app1
+  , Just (tc2, tys2) <- mb_tc_app2
+  , tc1 == tc2 || (tcIsStarKind ty1 && tcIsStarKind ty2)
+  = if isInjectiveTyCon tc1 Nominal
+    then unify_tys env tys1 tys2
+    else do { let inj | isTypeFamilyTyCon tc1
+                      = case familyTyConInjectivityInfo tc1 of
                                NotInjective -> repeat False
                                Injective bs -> bs
-                           | otherwise
-                           = repeat False
+                      | otherwise
+                      = repeat False
 
-                       (inj_tys1, noninj_tys1) = partitionByList inj tys1
-                       (inj_tys2, noninj_tys2) = partitionByList inj tys2
+                  (inj_tys1, noninj_tys1) = partitionByList inj tys1
+                  (inj_tys2, noninj_tys2) = partitionByList inj tys2
 
-                 ; unify_tys inj_tys1 inj_tys2
-                 ; inj_tf <- checkingInjectivity
-                 ; unless inj_tf $ -- See (end of) Note [Specification of unification]
-                   don'tBeSoSure $ unify_tys noninj_tys1 noninj_tys2 }
-    else -- tc1 /= tc2
-         if isGenerativeTyCon tc1 Nominal && isGenerativeTyCon tc2 Nominal
-         then surelyApart
-         else maybeApart
+            ; unify_tys env inj_tys1 inj_tys2
+            ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
+              don'tBeSoSure $ unify_tys env noninj_tys1 noninj_tys2 }
+
+  | Just (tc1, _) <- mb_tc_app1
+  , not (isGenerativeTyCon tc1 Nominal)
+    -- E.g.   unify_ty (F ty1) b  =  MaybeApart
+    --        because the (F ty1) behaves like a variable
+    --        NB: if unifying, we have already dealt
+    --            with the 'ty2 = variable' case
+  = maybeApart
+
+  | Just (tc2, _) <- mb_tc_app2
+  , not (isGenerativeTyCon tc2 Nominal)
+  , um_unif env
+    -- E.g.   unify_ty [a] (F ty2) =  MaybeApart, when unifying (only)
+    --        because the (F ty2) behaves like a variable
+    --        NB: we have already dealt with the 'ty1 = variable' case
+  = maybeApart
+
+  where
+    mb_tc_app1 = tcSplitTyConApp_maybe ty1
+    mb_tc_app2 = tcSplitTyConApp_maybe ty2
 
         -- Applications need a bit of care!
         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
         -- NB: we've already dealt with type variables,
         -- so if one type is an App the other one jolly well better be too
-unify_ty (AppTy ty1a ty1b) ty2 _kco
+unify_ty env (AppTy ty1a ty1b) ty2 _kco
   | Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
-  = unify_ty_app ty1a [ty1b] ty2a [ty2b]
+  = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
 
-unify_ty ty1 (AppTy ty2a ty2b) _kco
+unify_ty env ty1 (AppTy ty2a ty2b) _kco
   | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
-  = unify_ty_app ty1a [ty1b] ty2a [ty2b]
+  = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
 
-unify_ty (LitTy x) (LitTy y) _kco | x == y = return ()
+unify_ty (LitTy x) (LitTy y) _kco | x == y = return ()
 
-unify_ty (ForAllTy (TvBndr tv1 _) ty1) (ForAllTy (TvBndr tv2 _) ty2) kco
-  = do { unify_ty (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
-       ; umRnBndr2 tv1 tv2 $ unify_ty ty1 ty2 kco }
+unify_ty env (ForAllTy (TvBndr tv1 _) ty1) (ForAllTy (TvBndr tv2 _) ty2) kco
+  = do { unify_ty env (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
+       ; let env' = umRnBndr2 env tv1 tv2
+       ; unify_ty env' ty1 ty2 kco }
 
 -- See Note [Matching coercion variables]
-unify_ty (CoercionTy co1) (CoercionTy co2) kco
-  = do { unif <- amIUnifying
-       ; c_subst <- getCvSubstEnv
+unify_ty env (CoercionTy co1) (CoercionTy co2) kco
+  = do { c_subst <- getCvSubstEnv
        ; case co1 of
            CoVarCo cv
-             |  not unif
-             ,  not (cv `elemVarEnv` c_subst)
-             -> do { b <- tvBindFlagL cv
-                   ; if b == BindMe
-                       then do { checkRnEnvRCo co2
-                               ; let (co_l, co_r) = decomposeFunCo kco
-                                  -- cv :: t1 ~ t2
-                                  -- co2 :: s1 ~ s2
-                                  -- co_l :: t1 ~ s1
-                                  -- co_r :: t2 ~ s2
-                               ; extendCvEnv cv (co_l `mkTransCo`
-                                                 co2 `mkTransCo`
-                                                 mkSymCo co_r) }
-                       else return () }
+             | not (um_unif env)
+             , not (cv `elemVarEnv` c_subst)
+             , BindMe <- tvBindFlagL env cv
+             -> do { checkRnEnvRCo env co2
+                   ; let (co_l, co_r) = decomposeFunCo kco
+                      -- cv :: t1 ~ t2
+                      -- co2 :: s1 ~ s2
+                      -- co_l :: t1 ~ s1
+                      -- co_r :: t2 ~ s2
+                   ; extendCvEnv cv (co_l `mkTransCo`
+                                     co2 `mkTransCo`
+                                     mkSymCo co_r) }
            _ -> return () }
 
-unify_ty ty1 _ _
-  | Just (tc1, _) <- splitTyConApp_maybe ty1
-  , not (isGenerativeTyCon tc1 Nominal)
-  = maybeApart
-
-unify_ty _ ty2 _
-  | Just (tc2, _) <- splitTyConApp_maybe ty2
-  , not (isGenerativeTyCon tc2 Nominal)
-  = do { unif <- amIUnifying
-       ; if unif then maybeApart else surelyApart }
-
-unify_ty _ _ _ = surelyApart
+unify_ty _ _ _ _ = surelyApart
 
-unify_ty_app :: Type -> [Type] -> Type -> [Type] -> UM ()
-unify_ty_app ty1 ty1args ty2 ty2args
+unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
+unify_ty_app env ty1 ty1args ty2 ty2args
   | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
   , Just (ty2', ty2a) <- repSplitAppTy_maybe ty2
-  = unify_ty_app ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
+  = unify_ty_app env ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
 
   | otherwise
   = do { let ki1 = typeKind ty1
              ki2 = typeKind ty2
            -- See Note [Kind coercions in Unify]
-       ; unify_ty ki1 ki2 (mkNomReflCo liftedTypeKind)
-       ; unify_ty ty1 ty2 (mkNomReflCo ki1)
-       ; unify_tys ty1args ty2args }
+       ; unify_ty  env ki1 ki2 (mkNomReflCo liftedTypeKind)
+       ; unify_ty  env ty1 ty2 (mkNomReflCo ki1)
+       ; unify_tys env ty1args ty2args }
 
-unify_tys :: [Type] -> [Type] -> UM ()
-unify_tys orig_xs orig_ys
+unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
+unify_tys env orig_xs orig_ys
   = go orig_xs orig_ys
   where
     go []     []     = return ()
     go (x:xs) (y:ys)
       -- See Note [Kind coercions in Unify]
-      = do { unify_ty x y (mkNomReflCo $ typeKind x)
+      = do { unify_ty env x y (mkNomReflCo $ typeKind x)
            ; go xs ys }
     go _ _ = maybeApart  -- See Note [Lists of different lengths are MaybeApart]
 
 ---------------------------------
-uVar :: TyVar           -- Variable to be unified
+uVar :: UMEnv
+     -> TyVar           -- Variable to be unified
      -> Type            -- with this Type
      -> Coercion        -- :: kind tv ~N kind ty
      -> UM ()
 
-uVar tv1 ty kco
+uVar env tv1 ty kco
  = do { -- Check to see whether tv1 is refined by the substitution
         subst <- getTvSubstEnv
       ; case (lookupVarEnv subst tv1) of
-          Just ty' -> do { unif <- amIUnifying
-                         ; if unif
-                           then unify_ty ty' ty kco   -- Yes, call back into unify
-                           else -- when *matching*, we don't want to just recur here.
-                                -- this is because the range of the subst is the target
-                                -- type, not the template type. So, just check for
-                                -- normal type equality.
-                                guard ((ty' `mkCastTy` kco) `eqType` ty) }
-          Nothing  -> uUnrefined tv1 ty ty kco } -- No, continue
-
-uUnrefined :: TyVar             -- variable to be unified
+          Just ty' | um_unif env                 -- Unifying, so
+                   -> unify_ty env ty' ty kco   -- call back into unify
+                   | otherwise
+                   -> -- Matching, we don't want to just recur here.
+                      -- this is because the range of the subst is the target
+                      -- type, not the template type. So, just check for
+                      -- normal type equality.
+                      guard ((ty' `mkCastTy` kco) `eqType` ty)
+          Nothing  -> uUnrefined env tv1 ty ty kco } -- No, continue
+
+uUnrefined :: UMEnv
+           -> TyVar             -- variable to be unified
            -> Type              -- with this Type
            -> Type              -- (version w/ expanded synonyms)
            -> Coercion          -- :: kind tv ~N kind ty
@@ -922,36 +934,36 @@ uUnrefined :: TyVar             -- variable to be unified
 
 -- We know that tv1 isn't refined
 
-uUnrefined tv1 ty2 ty2' kco
+uUnrefined env tv1 ty2 ty2' kco
   | Just ty2'' <- coreView ty2'
-  = uUnrefined tv1 ty2 ty2'' kco    -- Unwrap synonyms
+  = uUnrefined env tv1 ty2 ty2'' kco    -- Unwrap synonyms
                 -- This is essential, in case we have
                 --      type Foo a = a
                 -- and then unify a ~ Foo a
 
   | TyVarTy tv2 <- ty2'
-  = do { tv1' <- umRnOccL tv1
-       ; tv2' <- umRnOccR tv2
-       ; unif <- amIUnifying
+  = do { let tv1' = umRnOccL env tv1
+             tv2' = umRnOccR env tv2
            -- See Note [Self-substitution when matching]
-       ; when (tv1' /= tv2' || not unif) $ do
+       ; when (tv1' /= tv2' || not (um_unif env)) $ do
        { subst <- getTvSubstEnv
           -- Check to see whether tv2 is refined
        ; case lookupVarEnv subst tv2 of
-         {  Just ty' | unif -> uUnrefined tv1 ty' ty' kco
-         ;  _               -> do
+         {  Just ty' | um_unif env -> uUnrefined env tv1 ty' ty' kco
+         ;  _                      -> do
        {   -- So both are unrefined
 
            -- And then bind one or the other,
            -- depending on which is bindable
-       ; b1 <- tvBindFlagL tv1
-       ; b2 <- tvBindFlagR tv2
-       ; let ty1 = mkTyVarTy tv1
+       ; let b1  = tvBindFlagL env tv1
+             b2  = tvBindFlagR env tv2
+             ty1 = mkTyVarTy tv1
        ; case (b1, b2) of
-           (BindMe, _)        -> do { checkRnEnvR ty2 -- make sure ty2 is not a local
-                                    ; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
-           (_, BindMe) | unif -> do { checkRnEnvL ty1 -- ditto for ty1
-                                    ; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
+           (BindMe, _) -> do { checkRnEnvR env ty2 -- make sure ty2 is not a local
+                             ; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
+           (_, BindMe) | um_unif env
+                       -> do { checkRnEnvL env ty1 -- ditto for ty1
+                             ; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
 
            _ | tv1' == tv2' -> return ()
              -- How could this happen? If we're only matching and if
@@ -960,12 +972,11 @@ uUnrefined tv1 ty2 ty2' kco
            _ -> maybeApart -- See Note [Unification with skolems]
   }}}}
 
-uUnrefined tv1 ty2 ty2' kco -- ty2 is not a type variable
+uUnrefined env tv1 ty2 ty2' kco -- ty2 is not a type variable
   = do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
-       ; unif   <- amIUnifying
-       ; if unif && occurs  -- See Note [Self-substitution when matching]
+       ; if um_unif env && occurs  -- See Note [Self-substitution when matching]
          then maybeApart       -- Occurs check, see Note [Fine-grained unification]
-         else do bindTv tv1 (ty2 `mkCastTy` mkSymCo kco) }
+         else do bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco) }
             -- Bind tyvar to the synonym if poss
 
 elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
@@ -973,11 +984,10 @@ elemNiSubstSet v set
   = do { tsubst <- getTvSubstEnv
        ; return $ v `elemVarSet` niSubstTvSet tsubst set }
 
-bindTv :: TyVar -> Type -> UM ()
-bindTv tv ty    -- ty is not a variable
-  = do  { checkRnEnvR ty -- make sure ty mentions no local variables
-        ; b <- tvBindFlagL tv
-        ; case b of
+bindTv :: UMEnv -> TyVar -> Type -> UM ()
+bindTv env tv ty    -- ty is not a variable
+  = do  { checkRnEnvR env ty -- make sure ty mentions no local variables
+        ; case tvBindFlagL env tv of
             Skolem -> maybeApart  -- See Note [Unification with skolems]
             BindMe -> extendTvEnv tv ty
         }
@@ -1006,147 +1016,125 @@ data BindFlag
 -}
 
 data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
-                       -- the user-supplied BindFlag function
-                   , um_unif     :: Bool   -- unification (True) or matching?
-                   , um_inj_tf   :: Bool   -- checking for injectivity?
-                             -- See (end of) Note [Specification of unification]
+                                       -- User-supplied BindFlag function
+                   , um_unif     :: AmIUnifying
+                   , um_inj_tf   :: Bool         -- Checking for injectivity?
+                          -- See (end of) Note [Specification of unification]
                    , um_rn_env   :: RnEnv2 }
 
 data UMState = UMState
                    { um_tv_env   :: TvSubstEnv
                    , um_cv_env   :: CvSubstEnv }
 
-newtype UM a = UM { unUM :: UMEnv -> UMState
-                         -> UnifyResultM (UMState, a) }
+newtype UM a = UM { unUM :: UMState -> UnifyResultM (UMState, a) }
 
 instance Functor UM where
       fmap = liftM
 
 instance Applicative UM where
-      pure a = UM (\s -> pure (s, a))
+      pure a = UM (\s -> pure (s, a))
       (<*>)  = ap
 
 instance Monad UM where
-  fail _   = UM (\_ -> SurelyApart) -- failed pattern match
-  m >>= k  = UM (\env state ->
-                  do { (state', v) <- unUM m env state
-                     ; unUM (k v) env state' })
+  fail _   = UM (\_ -> SurelyApart) -- failed pattern match
+  m >>= k  = UM (\state ->
+                  do { (state', v) <- unUM m state
+                     ; unUM (k v) state' })
 
 -- need this instance because of a use of 'guard' above
 instance Alternative UM where
-  empty     = UM (\_ -> Control.Applicative.empty)
-  m1 <|> m2 = UM (\env state ->
-                  unUM m1 env state <|>
-                  unUM m2 env state)
+  empty     = UM (\_ -> Control.Applicative.empty)
+  m1 <|> m2 = UM (\state ->
+                  unUM m1 state <|>
+                  unUM m2 state)
 
 instance MonadPlus UM
 
 #if __GLASGOW_HASKELL__ > 710
 instance MonadFail.MonadFail UM where
-    fail _   = UM (\_tvs _subst -> SurelyApart) -- failed pattern match
+    fail _   = UM (\_ -> SurelyApart) -- failed pattern match
 #endif
 
-initUM :: (TyVar -> BindFlag)
-       -> Bool        -- True <=> unify; False <=> match
-       -> Bool        -- True <=> doing an injectivity check
-       -> RnEnv2
-       -> TvSubstEnv  -- subst to extend
+initUM :: TvSubstEnv  -- subst to extend
        -> CvSubstEnv
        -> UM a -> UnifyResultM a
-initUM badtvs unif inj_tf rn_env subst_env cv_subst_env um
-  = case unUM um env state of
+initUM subst_env cv_subst_env um
+  = case unUM um state of
       Unifiable (_, subst)  -> Unifiable subst
       MaybeApart (_, subst) -> MaybeApart subst
       SurelyApart           -> SurelyApart
   where
-    env = UMEnv { um_bind_fun = badtvs
-                , um_unif     = unif
-                , um_inj_tf   = inj_tf
-                , um_rn_env   = rn_env }
     state = UMState { um_tv_env = subst_env
                     , um_cv_env = cv_subst_env }
 
-tvBindFlagL :: TyVar -> UM BindFlag
-tvBindFlagL tv = UM $ \env state ->
-  Unifiable (state, if inRnEnvL (um_rn_env env) tv
-                    then Skolem
-                    else um_bind_fun env tv)
+tvBindFlagL :: UMEnv -> TyVar -> BindFlag
+tvBindFlagL env tv
+  | inRnEnvL (um_rn_env env) tv = Skolem
+  | otherwise                   = um_bind_fun env tv
 
-tvBindFlagR :: TyVar -> UM BindFlag
-tvBindFlagR tv = UM $ \env state ->
-  Unifiable (state, if inRnEnvR (um_rn_env env) tv
-                    then Skolem
-                    else um_bind_fun env tv)
+tvBindFlagR :: UMEnv -> TyVar -> BindFlag
+tvBindFlagR env tv
+  | inRnEnvR (um_rn_env env) tv = Skolem
+  | otherwise                   = um_bind_fun env tv
 
 getTvSubstEnv :: UM TvSubstEnv
-getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
+getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
 
 getCvSubstEnv :: UM CvSubstEnv
-getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state)
+getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state)
 
 extendTvEnv :: TyVar -> Type -> UM ()
-extendTvEnv tv ty = UM $ \state ->
+extendTvEnv tv ty = UM $ \state ->
   Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
 
 extendCvEnv :: CoVar -> Coercion -> UM ()
-extendCvEnv cv co = UM $ \state ->
+extendCvEnv cv co = UM $ \state ->
   Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
 
-umRnBndr2 :: TyCoVar -> TyCoVar -> UM a -> UM a
-umRnBndr2 v1 v2 thing = UM $ \env state ->
-  let rn_env' = rnBndr2 (um_rn_env env) v1 v2 in
-  unUM thing (env { um_rn_env = rn_env' }) state
+umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
+umRnBndr2 env v1 v2
+  = env { um_rn_env = rnBndr2 (um_rn_env env) v1 v2 }
 
-checkRnEnv :: (RnEnv2 -> VarEnv Var) -> VarSet -> UM ()
-checkRnEnv get_set varset = UM $ \env state ->
+checkRnEnv :: (RnEnv2 -> VarEnv Var) -> UMEnv -> VarSet -> UM ()
+checkRnEnv get_set env varset = UM $ \ state ->
   let env_vars = get_set (um_rn_env env) in
   if isEmptyVarEnv env_vars || (getUniqSet varset `disjointVarEnv` env_vars)
      -- NB: That isEmptyVarSet is a critical optimization; it
      -- means we don't have to calculate the free vars of
      -- the type, often saving quite a bit of allocation.
-  then Unifiable (state, ())
+  then Unifiable  (state, ())
   else MaybeApart (state, ())
 
 -- | Converts any SurelyApart to a MaybeApart
 don'tBeSoSure :: UM () -> UM ()
-don'tBeSoSure um = UM $ \env state ->
-  case unUM um env state of
+don'tBeSoSure um = UM $ \ state ->
+  case unUM um state of
     SurelyApart -> MaybeApart (state, ())
     other       -> other
 
-checkRnEnvR :: Type -> UM ()
-checkRnEnvR ty = checkRnEnv rnEnvR (tyCoVarsOfType ty)
-
-checkRnEnvL :: Type -> UM ()
-checkRnEnvL ty = checkRnEnv rnEnvL (tyCoVarsOfType ty)
-
-checkRnEnvRCo :: Coercion -> UM ()
-checkRnEnvRCo co = checkRnEnv rnEnvR (tyCoVarsOfCo co)
+checkRnEnvR :: UMEnv -> Type -> UM ()
+checkRnEnvR env ty = checkRnEnv rnEnvR env (tyCoVarsOfType ty)
 
-umRnOccL :: TyVar -> UM TyVar
-umRnOccL v = UM $ \env state ->
-  Unifiable (state, rnOccL (um_rn_env env) v)
+checkRnEnvL :: UMEnv -> Type -> UM ()
+checkRnEnvL env ty = checkRnEnv rnEnvL env (tyCoVarsOfType ty)
 
-umRnOccR :: TyVar -> UM TyVar
-umRnOccR v = UM $ \env state ->
-  Unifiable (state, rnOccR (um_rn_env env) v)
+checkRnEnvRCo :: UMEnv -> Coercion -> UM ()
+checkRnEnvRCo env co = checkRnEnv rnEnvR env (tyCoVarsOfCo co)
 
-umSwapRn :: UM a -> UM a
-umSwapRn thing = UM $ \env state ->
-  let rn_env' = rnSwap (um_rn_env env) in
-  unUM thing (env { um_rn_env = rn_env' }) state
+umRnOccL :: UMEnv -> TyVar -> TyVar
+umRnOccL env v = rnOccL (um_rn_env env) v
 
-amIUnifying :: UM Bool
-amIUnifying = UM $ \env state -> Unifiable (state, um_unif env)
+umRnOccR :: UMEnv -> TyVar -> TyVar
+umRnOccR env v = rnOccR (um_rn_env env) v
 
-checkingInjectivity :: UM Bool
-checkingInjectivity = UM $ \env state -> Unifiable (state, um_inj_tf env)
+umSwapRn :: UMEnv -> UMEnv
+umSwapRn env = env { um_rn_env = rnSwap (um_rn_env env) }
 
 maybeApart :: UM ()
-maybeApart = UM (\state -> MaybeApart (state, ()))
+maybeApart = UM (\state -> MaybeApart (state, ()))
 
 surelyApart :: UM a
-surelyApart = UM (\_ -> SurelyApart)
+surelyApart = UM (\_ -> SurelyApart)
 
 {-
 %************************************************************************
diff --git a/testsuite/tests/indexed-types/should_compile/T13705.hs b/testsuite/tests/indexed-types/should_compile/T13705.hs
new file mode 100644 (file)
index 0000000..770f508
--- /dev/null
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+module T13705 where
+
+data D x
+
+type family F t = s | s -> t
+type instance F (D t) = D (F t)
+
+f :: F s -> ()
+f _ = ()
+
+g :: D (F t) -> ()
+g x = f x
+
index 00d40ce..ec55113 100644 (file)
@@ -264,3 +264,4 @@ test('T13244', normal, compile, [''])
 test('T13398a', normal, compile, [''])
 test('T13398b', normal, compile, [''])
 test('T13662', normal, compile, [''])
+test('T13705', normal, compile, [''])