+ Updating tau types
+%* *
+%************************************************************************
+
+Can't be in TcUnify, as we also need it in TcTyFuns.
+
+\begin{code}
+type SwapFlag = Bool
+ -- False <=> the two args are (actual, expected) respectively
+ -- True <=> the two args are (expected, actual) respectively
+
+checkUpdateMeta :: SwapFlag
+ -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+-- Update tv1, which is flexi; occurs check is alrady done
+-- The 'check' version does a kind check too
+-- We do a sub-kind check here: we might unify (a b) with (c d)
+-- where b::*->* and d::*; this should fail
+
+checkUpdateMeta swapped tv1 ref1 ty2
+ = do { checkKinds swapped tv1 ty2
+ ; updateMeta tv1 ref1 ty2 }
+
+updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+updateMeta tv1 ref1 ty2
+ = ASSERT( isMetaTyVar tv1 )
+ ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
+ do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
+ ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
+ ; writeMutVar ref1 (Indirect ty2)
+ }
+
+----------------
+checkKinds :: Bool -> TyVar -> Type -> TcM ()
+checkKinds swapped tv1 ty2
+-- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
+-- ty2 has been zonked at this stage, which ensures that
+-- its kind has as much boxity information visible as possible.
+ | tk2 `isSubKind` tk1 = return ()
+
+ | otherwise
+ -- Either the kinds aren't compatible
+ -- (can happen if we unify (a b) with (c d))
+ -- or we are unifying a lifted type variable with an
+ -- unlifted type: e.g. (id 3#) is illegal
+ = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
+ unifyKindMisMatch k1 k2
+ where
+ (k1,k2) | swapped = (tk2,tk1)
+ | otherwise = (tk1,tk2)
+ tk1 = tyVarKind tv1
+ tk2 = typeKind ty2
+
+----------------
+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)
+-- (b) that ty is a monotype
+-- Furthermore, in the interest of (b), if you find an
+-- empty box (BoxTv that is Flexi), fill it in with a TauTv
+--
+-- 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
+ = 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' <- mapM go tys
+ ; return $ occurs (TyConApp tc) tys' }
+ 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 _ _) = notMonoType orig_ty -- (b)
+
+ go (TyVarTy tv)
+ | orig_tv == tv = return $ Left False -- (a)
+ | isTcTyVar tv = go_tyvar tv (tcTyVarDetails 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 $ 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 $ 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 -> do { ty <- fillBoxWithTau tv ref
+ ; return $ Right ty }
+ _ -> return $ Right (TyVarTy tv)
+ }
+
+ -- go_syn is called for synonyms only
+ -- See Note [Type synonyms and the occur check]
+ go_syn tc tys
+ | not (isTauTyCon tc)
+ = notMonoType orig_ty -- (b) again
+ | otherwise
+ = do { (_msgs, mb_tys') <- tryTc (mapM go tys)
+ ; case mb_tys' of
+
+ -- 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)
+ }
+
+ -- 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
+-- tau-type meta-variable, whose print-name is the same as tv
+-- Choosing the same name is good: when we instantiate a function
+-- we allocate boxy tyvars with the same print-name as the quantified
+-- tyvar; and then we often fill the box with a tau-tyvar, and again
+-- we want to choose the same name.
+fillBoxWithTau tv ref
+ = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget
+ ; let tau = mkTyVarTy tv' -- name of the type variable
+ ; writeMutVar ref (Indirect tau)
+ ; 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).
+
+--------------
+
+Execute a bag of type variable bindings.
+
+\begin{code}
+execTcTyVarBinds :: TcTyVarBinds -> TcM ()
+execTcTyVarBinds = mapM_ execTcTyVarBind . bagToList
+ where
+ execTcTyVarBind (TcTyVarBind tv ty)
+ = do { ASSERTM2( do { details <- readMetaTyVar tv
+ ; return (isFlexi details) }, ppr tv )
+ ; ty' <- if isCoVar tv
+ then return ty
+ else do { maybe_ty <- checkTauTvUpdate tv ty
+ ; case maybe_ty of
+ Nothing -> pprPanic "TcRnMonad.execTcTyBind"
+ (ppr tv <+> text ":=" <+> ppr ty)
+ Just ty' -> return ty'
+ }
+ ; writeMetaTyVar tv ty'
+ }
+\end{code}
+
+Error mesages in case of kind mismatch.
+
+\begin{code}
+unifyKindMisMatch :: TcKind -> TcKind -> TcM ()
+unifyKindMisMatch ty1 ty2 = do
+ ty1' <- zonkTcKind ty1
+ ty2' <- zonkTcKind ty2
+ let
+ msg = hang (ptext (sLit "Couldn't match kind"))
+ 2 (sep [quotes (ppr ty1'),
+ ptext (sLit "against"),
+ quotes (ppr ty2')])
+ failWithTc msg
+
+unifyKindCtxt :: Bool -> TyVar -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)
+unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
+ -- tv1 and ty2 are zonked already
+ = return msg
+ where
+ msg = (env2, ptext (sLit "When matching the kinds of") <+>
+ sep [quotes pp_expected <+> ptext (sLit "and"), quotes pp_actual])
+
+ (pp_expected, pp_actual) | swapped = (pp2, pp1)
+ | otherwise = (pp1, pp2)
+ (env1, tv1') = tidyOpenTyVar tidy_env tv1
+ (env2, ty2') = tidyOpenType env1 ty2
+ pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
+ pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
+\end{code}
+
+Error message for failure due to an occurs check.
+
+\begin{code}
+occurCheckErr :: TcType -> TcType -> TcM a
+occurCheckErr ty containingTy
+ = do { env0 <- tcInitTidyEnv
+ ; ty' <- zonkTcType ty
+ ; containingTy' <- zonkTcType containingTy
+ ; let (env1, tidy_ty1) = tidyOpenType env0 ty'
+ (env2, tidy_ty2) = tidyOpenType env1 containingTy'
+ extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
+ ; failWithTcM (env2, hang msg 2 extra) }
+ where
+ msg = ptext (sLit "Occurs check: cannot construct the infinite type:")
+\end{code}
+
+%************************************************************************
+%* *
projects / ghc-hetmet.git / blobdiff