From: Manuel M T Chakravarty Date: Sun, 16 Sep 2007 13:04:19 +0000 (+0000) Subject: FIX: TypeFamilies: should_compile/Simple12 X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=1b6b0ba3b93351045e19df9fa9cb0f8baf033afc FIX: TypeFamilies: should_compile/Simple12 - checkTauTvUpdate now distinguishes between whether (1) a type variables occurs only in type family parameters (in which case unification is to be deferred) (2) other variable occurences (which case we fail with a cannot create infinite type message, as before) --- diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 13fbf55..f14cf59 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -177,7 +177,7 @@ checkKinds swapped tv1 ty2 tk2 = typeKind ty2 ---------------- -checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType +checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) -- (checkTauTvUpdate tv ty) -- We are about to update the TauTv tv with ty. -- Check (a) that tv doesn't occur in ty (occurs check) @@ -185,42 +185,79 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType -- Furthermore, in the interest of (b), if you find an -- empty box (BoxTv that is Flexi), fill it in with a TauTv -- --- Returns the (non-boxy) type to update the type variable with, or fails +-- We have three possible outcomes: +-- (1) Return the (non-boxy) type to update the type variable with, +-- [we know the update is ok!] +-- (2) return Nothing, or +-- [we cannot tell whether the update is ok right now] +-- (3) fails. +-- [the update is definitely invalid] +-- We return Nothing in case the tv occurs in ty *under* a type family +-- application. In this case, we must not update tv (to avoid a cyclic type +-- term), but we also cannot fail claiming an infinite type. Given +-- type family F a +-- type instance F Int = Int +-- consider +-- a ~ F a +-- This is perfectly reasonable, if we later get a ~ Int. checkTauTvUpdate orig_tv orig_ty - = go orig_ty + = do { result <- go orig_ty + ; case result of + Right ty -> return $ Just ty + Left True -> return $ Nothing + Left False -> occurCheckErr (mkTyVarTy orig_tv) orig_ty + } where + go :: TcType -> TcM (Either Bool TcType) + -- go returns + -- Right ty if everything is fine + -- Left True if orig_tv occurs in orig_ty, but under a type family app + -- Left False if orig_tv occurs in orig_ty (with no type family app) + -- It fails if it encounters a forall type, except as an argument for a + -- closed type synonym that expands to a tau type. go (TyConApp tc tys) | isSynTyCon tc = go_syn tc tys - | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') } + | otherwise = do { tys' <- mappM go tys + ; return $ occurs (TyConApp tc) tys' } go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations - go (PredTy p) = do { p' <- go_pred p; return (PredTy p') } - go (FunTy arg res) = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') } - go (AppTy fun arg) = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') } + go (PredTy p) = do { p' <- go_pred p + ; return $ occurs1 PredTy p' } + go (FunTy arg res) = do { arg' <- go arg + ; res' <- go res + ; return $ occurs2 FunTy arg' res' } + go (AppTy fun arg) = do { fun' <- go fun + ; arg' <- go arg + ; return $ occurs2 mkAppTy fun' arg' } -- NB the mkAppTy; we might have instantiated a -- type variable to a type constructor, so we need -- to pull the TyConApp to the top. go (ForAllTy tv ty) = notMonoType orig_ty -- (b) go (TyVarTy tv) - | orig_tv == tv = occurCheck tv -- (a) + | orig_tv == tv = return $ Left False -- (a) | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv) - | otherwise = return (TyVarTy tv) + | otherwise = return $ Right (TyVarTy tv) -- Ordinary (non Tc) tyvars -- occur inside quantified types - go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') } - go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') } - go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') } + go_pred (ClassP c tys) = do { tys' <- mapM go tys + ; return $ occurs (ClassP c) tys' } + go_pred (IParam n ty) = do { ty' <- go ty + ; return $ occurs1 (IParam n) ty' } + go_pred (EqPred t1 t2) = do { t1' <- go t1 + ; t2' <- go t2 + ; return $ occurs2 EqPred t1' t2' } - go_tyvar tv (SkolemTv _) = return (TyVarTy tv) + go_tyvar tv (SkolemTv _) = return $ Right (TyVarTy tv) go_tyvar tv (MetaTv box ref) = do { cts <- readMutVar ref ; case cts of Indirect ty -> go ty Flexi -> case box of - BoxTv -> fillBoxWithTau tv ref - other -> return (TyVarTy tv) + BoxTv -> do { ty <- fillBoxWithTau tv ref + ; return $ Right ty } + other -> return $ Right (TyVarTy tv) } -- go_syn is called for synonyms only @@ -231,18 +268,40 @@ checkTauTvUpdate orig_tv orig_ty | otherwise = do { (msgs, mb_tys') <- tryTc (mapM go tys) ; case mb_tys' of - Just tys' -> return (TyConApp tc tys') - -- Retain the synonym (the common case) - Nothing | isOpenTyCon tc - -> notMonoArgs (TyConApp tc tys) - -- Synonym families must have monotype args - | otherwise - -> go (expectJust "checkTauTvUpdate" - (tcView (TyConApp tc tys))) - -- Try again, expanding the synonym + + -- we had a type error => forall in type parameters + Nothing + | isOpenTyCon tc -> notMonoArgs (TyConApp tc tys) + -- Synonym families must have monotype args + | otherwise -> go (expectJust "checkTauTvUpdate(1)" + (tcView (TyConApp tc tys))) + -- Try again, expanding the synonym + + -- no type error, but need to test whether occurs check happend + Just tys' -> + case occurs id tys' of + Left _ + | isOpenTyCon tc -> return $ Left True + -- Variable occured under type family application + | otherwise -> go (expectJust "checkTauTvUpdate(2)" + (tcView (TyConApp tc tys))) + -- Try again, expanding the synonym + Right raw_tys' -> return $ Right (TyConApp tc raw_tys') + -- Retain the synonym (the common case) } - occurCheck tv = occurCheckErr (mkTyVarTy tv) orig_ty + -- Left results (= occurrence of orig_ty) dominate and + -- (Left False) (= fatal occurrence) dominates over (Left True) + occurs :: ([a] -> b) -> [Either Bool a] -> Either Bool b + occurs c = either Left (Right . c) . foldr combine (Right []) + where + combine (Left famInst1) (Left famInst2) = Left (famInst1 && famInst2) + combine (Right _ ) (Left famInst) = Left famInst + combine (Left famInst) (Right _) = Left famInst + combine (Right arg) (Right args) = Right (arg:args) + + occurs1 c x = occurs (\[x'] -> c x') [x] + occurs2 c x y = occurs (\[x', y'] -> c x' y') [x, y] fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType -- (fillBoxWithTau tv ref) fills ref with a freshly allocated @@ -258,6 +317,28 @@ fillBoxWithTau tv ref ; return tau } \end{code} +Note [Type synonyms and the occur check] +~~~~~~~~~~~~~~~~~~~~ +Basically we want to update tv1 := ps_ty2 +because ps_ty2 has type-synonym info, which improves later error messages + +But consider + type A a = () + + f :: (A a -> a -> ()) -> () + f = \ _ -> () + + x :: () + x = f (\ x p -> p x) + +In the application (p x), we try to match "t" with "A t". If we go +ahead and bind t to A t (= ps_ty2), we'll lead the type checker into +an infinite loop later. +But we should not reject the program, because A t = (). +Rather, we should bind t to () (= non_var_ty2). + +-------------- + Error mesages in case of kind mismatch. \begin{code} diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 64c9830..126a029 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -953,10 +953,14 @@ unifyMetaRule insts -- updatable meta variable meets non-variable type -- => occurs check, monotype check, and kinds match check, then update uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv - = do { ty' <- checkTauTvUpdate tv ty -- occurs + monotype check - ; checkUpdateMeta swapped tv ref ty' -- update meta var - ; writeMetaTyVar cotv ty' -- update the co var - ; return ([], True) + = do { mb_ty' <- checkTauTvUpdate tv ty -- occurs + monotype check + ; case mb_ty' of + Nothing -> return ([inst], False) -- tv occurs in faminst + Just ty' -> + do { checkUpdateMeta swapped tv ref ty' -- update meta var + ; writeMetaTyVar cotv ty' -- update co var + ; return ([], True) + } } uMeta _ _ _ _ _ = panic "uMeta" diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index f188af1..233e87d 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -1318,12 +1318,10 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2 = -- ty2 is not a type variable case details1 of - MetaTv (SigTv _) _ -> rigid_variable - MetaTv info ref1 -> - do { uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2 - ; return IdCo - } - SkolemTv _ -> rigid_variable + MetaTv (SigTv _) _ -> rigid_variable + MetaTv info ref1 -> + uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2 + SkolemTv _ -> rigid_variable where rigid_variable | isOpenSynTyConApp non_var_ty2 @@ -1399,14 +1397,15 @@ defer_unification outer False ty1 ty2 ; return $ ACo $ TyVarTy cotv } ---------------- -uMetaVar :: SwapFlag +uMetaVar :: Bool -- pop innermost context? + -> SwapFlag -> TcTyVar -> BoxInfo -> IORef MetaDetails -> TcType -> TcType - -> TcM () + -> TcM CoercionI -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau) -- ty2 is not a type variable -uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 +uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 = -- tv1 is a BoxTv. So we must unbox ty2, to ensure -- that any boxes in ty2 are filled with monotypes -- @@ -1422,11 +1421,21 @@ uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 return () -- This really should *not* happen Flexi -> return () #endif - ; checkUpdateMeta swapped tv1 ref1 final_ty } + ; checkUpdateMeta swapped tv1 ref1 final_ty + ; return IdCo + } -uMetaVar swapped tv1 info1 ref1 ps_ty2 non_var_ty2 - = do { final_ty <- checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check - ; checkUpdateMeta swapped tv1 ref1 final_ty } +uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2 + = do { -- Occurs check + monotype check + ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2 + ; case mb_final_ty of + Nothing -> -- tv1 occured in type family parameter + defer_unification outer swapped (mkTyVarTy tv1) ps_ty2 + Just final_ty -> + do { checkUpdateMeta swapped tv1 ref1 final_ty + ; return IdCo + } + } ---------------- uUnfilledVars :: Outer @@ -1505,26 +1514,6 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) -- a user-written type sig \end{code} -Note [Type synonyms and the occur check] -~~~~~~~~~~~~~~~~~~~~ -Basically we want to update tv1 := ps_ty2 -because ps_ty2 has type-synonym info, which improves later error messages - -But consider - type A a = () - - f :: (A a -> a -> ()) -> () - f = \ _ -> () - - x :: () - x = f (\ x p -> p x) - -In the application (p x), we try to match "t" with "A t". If we go -ahead and bind t to A t (= ps_ty2), we'll lead the type checker into -an infinite loop later. -But we should not reject the program, because A t = (). -Rather, we should bind t to () (= non_var_ty2). - \begin{code} refineBox :: TcType -> TcM TcType -- Unbox the outer box of a boxy type (if any)