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)
-- 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
| 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
; 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}
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
; 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
--
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
-- 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)
projects / ghc-hetmet.git / commitdiff