newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newKindVar, newKindVars,
lookupTcTyVar, LookupTyVarResult(..),
- newMetaTyVar, readMetaTyVar, writeMetaTyVar,
+
+ newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar,
--------------------------------
-- Boxy type variables
--------------------------------
-- Creating new coercion variables
- newCoVars,
+ newCoVars, newMetaCoVar,
--------------------------------
-- Instantiation
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
- tcInstSigTyVars, zonkSigTyVar,
+ tcInstSigTyVars,
tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
- tcSkolSigType, tcSkolSigTyVars,
+ tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
--------------------------------
-- Checking type validity
- Rank, UserTypeCtxt(..), checkValidType,
+ Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
- checkValidInstHead, checkValidInstance, checkAmbiguity,
+ checkValidInstHead, checkValidInstance,
checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
- validDerivPred, arityErr,
+ checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
+ unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
--------------------------------
-- Zonking
zonkType, zonkTcPredType,
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
+ zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
-> TcType -- Type to instantiate
-> TcM ([TcTyVar], TcThetaType, TcType) -- Result
+ -- (type vars (excl coercion vars), preds (incl equalities), rho)
tcInstType inst_tyvars ty
= case tcSplitForAllTys ty of
([], rho) -> let -- There may be overloading despite no type variables;
%************************************************************************
%* *
+ 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 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 = returnM ()
+
+ | 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' <- 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 $ 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 = 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 }
+ other -> 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).
+
+--------------
+
+Error mesages in case of kind mismatch.
+
+\begin{code}
+unifyKindMisMatch ty1 ty2
+ = zonkTcKind ty1 `thenM` \ ty1' ->
+ zonkTcKind ty2 `thenM` \ ty2' ->
+ let
+ msg = hang (ptext SLIT("Couldn't match kind"))
+ 2 (sep [quotes (ppr ty1'),
+ ptext SLIT("against"),
+ quotes (ppr ty2')])
+ in
+ failWithTc msg
+
+unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
+ -- tv1 and ty2 are zonked already
+ = returnM 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}
+
+%************************************************************************
+%* *
Kind variables
%* *
%************************************************************************
(mkCoKind ty1 ty2)
| ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
+newMetaCoVar :: TcType -> TcType -> TcM TcTyVar
+newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2)
+
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
; ref <- newMutVar Flexi
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
readMutVar (metaTvRef tyvar)
+isFilledMetaTyVar :: TyVar -> TcM Bool
+-- True of a filled-in (Indirect) meta type variable
+isFilledMetaTyVar tv
+ | not (isTcTyVar tv) = return False
+ | MetaTv _ ref <- tcTyVarDetails tv
+ = do { details <- readMutVar ref
+ ; return (isIndirect details) }
+ | otherwise = return False
+
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
#ifndef DEBUG
writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
k = tyVarKind tv
default_k = defaultKind k
-zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
+zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
-zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
+zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
--
-- The quantified type variables often include meta type variables
-- we want to freeze them into ordinary type variables, and
-- default their kind (e.g. from OpenTypeKind to TypeKind)
-- -- see notes with Kind.defaultKind
--- The meta tyvar is updated to point to the new regular TyVar. Now any
+-- The meta tyvar is updated to point to the new skolem TyVar. Now any
-- bound occurences of the original type variable will get zonked to
-- the immutable version.
--
| otherwise -- It's a meta-type-variable
= do { details <- readMetaTyVar tv
- -- Create the new, frozen, regular type variable
+ -- Create the new, frozen, skolem type variable
+ -- We zonk to a skolem, not to a regular TcVar
+ -- See Note [Zonking to Skolem]
; let final_kind = defaultKind (tyVarKind tv)
- final_tv = mkTyVar (tyVarName tv) final_kind
+ final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
-- Bind the meta tyvar to the new tyvar
; case details of
; return final_tv }
\end{code}
-[Silly Type Synonyms]
-
+Note [Silly Type Synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
type C u a = u -- Note 'a' unused
All very silly. I think its harmless to ignore the problem. We'll end up with
a /\a in the final result but all the occurrences of a will be zonked to ()
+Note [Zonking to Skolem]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We used to zonk quantified type variables to regular TyVars. However, this
+leads to problems. Consider this program from the regression test suite:
+
+ eval :: Int -> String -> String -> String
+ eval 0 root actual = evalRHS 0 root actual
+
+ evalRHS :: Int -> a
+ evalRHS 0 root actual = eval 0 root actual
+
+It leads to the deferral of an equality
+
+ (String -> String -> String) ~ a
+
+which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
+In the meantime `a' is zonked and quantified to form `evalRHS's signature.
+This has the *side effect* of also zonking the `a' in the deferred equality
+(which at this point is being handed around wrapped in an implication
+constraint).
+
+Finally, the equality (with the zonked `a') will be handed back to the
+simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
+If we zonk `a' with a regular type variable, we will have this regular type
+variable now floating around in the simplifier, which in many places assumes to
+only see proper TcTyVars.
+
+We can avoid this problem by zonking with a skolem. The skolem is rigid
+(which we requirefor a quantified variable), but is still a TcTyVar that the
+simplifier knows how to deal with.
+
%************************************************************************
%* *
-- Checks that the type is valid for the given context
checkValidType ctxt ty
= traceTc (text "checkValidType" <+> ppr ty) `thenM_`
- doptM Opt_UnboxedTuples `thenM` \ unboxed ->
- doptM Opt_Rank2Types `thenM` \ rank2 ->
- doptM Opt_RankNTypes `thenM` \ rankn ->
+ doptM Opt_UnboxedTuples `thenM` \ unboxed ->
+ doptM Opt_Rank2Types `thenM` \ rank2 ->
+ doptM Opt_RankNTypes `thenM` \ rankn ->
doptM Opt_PolymorphicComponents `thenM` \ polycomp ->
let
rank | rankn = Arbitrary
checkTc kind_ok (kindErr actual_kind) `thenM_`
-- Check the internal validity of the type itself
- check_poly_type rank ubx_tup ty `thenM_`
+ check_type rank ubx_tup ty `thenM_`
traceTc (text "checkValidType done" <+> ppr ty)
+
+checkValidMonoType :: Type -> TcM ()
+checkValidMonoType ty = check_mono_type ty
\end{code}
decRank Arbitrary = Arbitrary
decRank (Rank n) = Rank (n-1)
+nonZeroRank :: Rank -> Bool
+nonZeroRank (Rank 0) = False
+nonZeroRank _ = True
+
----------------------------------------
data UbxTupFlag = UT_Ok | UT_NotOk
-- The "Ok" version means "ok if -fglasgow-exts is on"
----------------------------------------
-check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
-check_poly_type (Rank 0) ubx_tup ty
- = check_tau_type (Rank 0) ubx_tup ty
-
-check_poly_type rank ubx_tup ty
- | null tvs && null theta
- = check_tau_type rank ubx_tup ty
- | otherwise
- = do { check_valid_theta SigmaCtxt theta
- ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
+check_mono_type :: Type -> TcM () -- No foralls anywhere
+ -- No unlifted types of any kind
+check_mono_type ty
+ = do { check_type (Rank 0) UT_NotOk ty
+ ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
+
+check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+-- The args say what the *type* context requires, independent
+-- of *flag* settings. You test the flag settings at usage sites.
+--
+-- Rank is allowed rank for function args
+-- Rank 0 means no for-alls anywhere
+
+check_type rank ubx_tup ty
+ | not (null tvs && null theta)
+ = do { checkTc (nonZeroRank rank) (forAllTyErr ty)
+ -- Reject e.g. (Maybe (?x::Int => Int)),
+ -- with a decent error message
+ ; check_valid_theta SigmaCtxt theta
+ ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
; checkFreeness tvs theta
; checkAmbiguity tvs theta (tyVarsOfType tau) }
where
(tvs, theta, tau) = tcSplitSigmaTy ty
-----------------------------------------
-check_arg_type :: Type -> TcM ()
--- The sort of type that can instantiate a type variable,
--- or be the argument of a type constructor.
--- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
--- Other unboxed types are very occasionally allowed as type
--- arguments depending on the kind of the type constructor
---
--- For example, we want to reject things like:
---
--- instance Ord a => Ord (forall s. T s a)
--- and
--- g :: T s (forall b.b)
---
--- NB: unboxed tuples can have polymorphic or unboxed args.
--- This happens in the workers for functions returning
--- product types with polymorphic components.
--- But not in user code.
--- Anyway, they are dealt with by a special case in check_tau_type
-
-check_arg_type ty
- = check_poly_type Arbitrary UT_NotOk ty `thenM_`
- checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
-
-----------------------------------------
-check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
--- Rank is allowed rank for function args
--- No foralls otherwise
-
-check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
- -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
-
-- Naked PredTys don't usually show up, but they can as a result of
-- {-# SPECIALISE instance Ord Char #-}
-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
-- are handled, but the quick thing is just to permit PredTys here.
-check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
- check_pred_ty dflags TypeCtxt sty
-
-check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
-check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
- = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
- check_poly_type rank UT_Ok res_ty
-
-check_tau_type rank ubx_tup (AppTy ty1 ty2)
- = check_arg_type ty1 `thenM_` check_arg_type ty2
-
-check_tau_type rank ubx_tup (NoteTy other_note ty)
- = check_tau_type rank ubx_tup ty
-
-check_tau_type rank ubx_tup ty@(TyConApp tc tys)
- | isSynTyCon tc
- = do { -- It's OK to have an *over-applied* type synonym
+check_type rank ubx_tup (PredTy sty)
+ = do { dflags <- getDOpts
+ ; check_pred_ty dflags TypeCtxt sty }
+
+check_type rank ubx_tup (TyVarTy _) = returnM ()
+check_type rank ubx_tup ty@(FunTy arg_ty res_ty)
+ = do { check_type (decRank rank) UT_NotOk arg_ty
+ ; check_type rank UT_Ok res_ty }
+
+check_type rank ubx_tup (AppTy ty1 ty2)
+ = do { check_arg_type rank ty1
+ ; check_arg_type rank ty2 }
+
+check_type rank ubx_tup (NoteTy other_note ty)
+ = check_type rank ubx_tup ty
+
+check_type rank ubx_tup ty@(TyConApp tc tys)
+ | isSynTyCon tc
+ = do { -- Check that the synonym has enough args
+ -- This applies equally to open and closed synonyms
+ -- It's OK to have an *over-applied* type synonym
-- data Tree a b = ...
-- type Foo a = Tree [a]
-- f :: Foo a b -> ...
- ; case tcView ty of
- Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
- Nothing -> unless (isOpenTyCon tc -- No expansion if open
- && tyConArity tc <= length tys) $
- failWithTc arity_msg
-
- ; ok <- doptM Opt_PartiallyAppliedClosedTypeSynonyms
- ; if ok && not (isOpenTyCon tc) then
- -- Don't check the type arguments of *closed* synonyms.
- -- This allows us to instantiate a synonym defn with a
- -- for-all type, or with a partially-applied type synonym.
- -- e.g. type T a b = a
- -- type S m = m ()
- -- f :: S (T Int)
- -- Here, T is partially applied, so it's illegal in H98.
- -- But if you expand S first, then T we get just
- -- f :: Int
- -- which is fine.
- returnM ()
- else
- -- For H98, do check the type args
- mappM_ check_arg_type tys
- }
+ checkTc (tyConArity tc <= length tys) arity_msg
+
+ -- See Note [Liberal type synonyms]
+ ; liberal <- doptM Opt_LiberalTypeSynonyms
+ ; if not liberal || isOpenSynTyCon tc then
+ -- For H98 and synonym families, do check the type args
+ mappM_ check_mono_type tys
+
+ else -- In the liberal case (only for closed syns), expand then check
+ case tcView ty of
+ Just ty' -> check_type rank ubx_tup ty'
+ Nothing -> pprPanic "check_tau_type" (ppr ty)
+ }
| isUnboxedTupleTyCon tc
- = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed ->
- checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg `thenM_`
- mappM_ (check_tau_type (Rank 0) UT_Ok) tys
- -- Args are allowed to be unlifted, or
+ = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples
+ ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
+
+ ; impred <- doptM Opt_ImpredicativeTypes
+ ; let rank' = if impred then rank else Rank 0
+ -- c.f. check_arg_type
+ -- However, args are allowed to be unlifted, or
-- more unboxed tuples, so can't use check_arg_ty
+ ; mappM_ (check_type rank' UT_Ok) tys }
| otherwise
- = mappM_ check_arg_type tys
+ = mappM_ (check_arg_type rank) tys
where
ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
ubx_tup_msg = ubxArgTyErr ty
----------------------------------------
+check_arg_type :: Rank -> Type -> TcM ()
+-- The sort of type that can instantiate a type variable,
+-- or be the argument of a type constructor.
+-- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
+-- Other unboxed types are very occasionally allowed as type
+-- arguments depending on the kind of the type constructor
+--
+-- For example, we want to reject things like:
+--
+-- instance Ord a => Ord (forall s. T s a)
+-- and
+-- g :: T s (forall b.b)
+--
+-- NB: unboxed tuples can have polymorphic or unboxed args.
+-- This happens in the workers for functions returning
+-- product types with polymorphic components.
+-- But not in user code.
+-- Anyway, they are dealt with by a special case in check_tau_type
+
+check_arg_type rank ty
+ = do { impred <- doptM Opt_ImpredicativeTypes
+ ; let rank' = if impred then rank else Rank 0 -- Monotype unless impredicative
+ ; check_type rank' UT_NotOk ty
+ ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
+
+----------------------------------------
forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
-unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
+unliftedArgErr ty = ptext SLIT("Illegal unlifted type:") <+> ppr ty
ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
\end{code}
+Note [Liberal type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
+doing validity checking. This allows us to instantiate a synonym defn
+with a for-all type, or with a partially-applied type synonym.
+ e.g. type T a b = a
+ type S m = m ()
+ f :: S (T Int)
+Here, T is partially applied, so it's illegal in H98. But if you
+expand S first, then T we get just
+ f :: Int
+which is fine.
+
+IMPORTANT: suppose T is a type synonym. Then we must do validity
+checking on an appliation (T ty1 ty2)
+
+ *either* before expansion (i.e. check ty1, ty2)
+ *or* after expansion (i.e. expand T ty1 ty2, and then check)
+ BUT NOT BOTH
+
+If we do both, we get exponential behaviour!!
+
+ data TIACons1 i r c = c i ::: r c
+ type TIACons2 t x = TIACons1 t (TIACons1 t x)
+ type TIACons3 t x = TIACons2 t (TIACons1 t x)
+ type TIACons4 t x = TIACons2 t (TIACons2 t x)
+ type TIACons7 t x = TIACons4 t (TIACons3 t x)
%************************************************************************
; checkTc (arity == n_tys) arity_err
-- Check the form of the argument types
- ; mappM_ check_arg_type tys
+ ; mappM_ check_mono_type tys
; checkTc (check_class_pred_tys dflags ctxt tys)
(predTyVarErr pred $$ how_to_allow)
}
; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
-- Check the form of the argument types
- ; check_eq_arg_type ty1
- ; check_eq_arg_type ty2
+ ; check_mono_type ty1
+ ; check_mono_type ty2
}
- where
- check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
-check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
+check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_mono_type ty
-- Implicit parameters only allowed in type
-- signatures; not in instance decls, superclasses etc
-- The reason for not allowing implicit params in instances is a bit
don't need to check for ambiguity either, because the test can't fail
(see is_ambig).
+
\begin{code}
checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
checkAmbiguity forall_tyvars theta tau_tyvars
complain pred = addErrTc (ambigErr pred)
extended_tau_vars = grow theta tau_tyvars
- -- Only a *class* predicate can give rise to ambiguity
- -- An *implicit parameter* cannot. For example:
- -- foo :: (?x :: [a]) => Int
- -- foo = length ?x
- -- is fine. The call site will suppply a particular 'x'
+ -- See Note [Implicit parameters and ambiguity] in TcSimplify
is_ambig pred = isClassPred pred &&
any ambig_var (varSetElems (tyVarsOfPred pred))
n_arguments | n == 0 = ptext SLIT("no arguments")
| n == 1 = ptext SLIT("1 argument")
| True = hsep [int n, ptext SLIT("arguments")]
+
+-----------------
+notMonoType ty
+ = do { ty' <- zonkTcType ty
+ ; env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+ msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
+ ; failWithTcM (env1, msg) }
+
+notMonoArgs ty
+ = do { ty' <- zonkTcType ty
+ ; env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+ msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
+ ; failWithTcM (env1, msg) }
\end{code}
Just (clas,tys) ->
getDOpts `thenM` \ dflags ->
- mappM_ check_arg_type tys `thenM_`
+ mappM_ check_mono_type tys `thenM_`
check_inst_head dflags clas tys `thenM_`
returnM (clas, tys)
}}
checkTc (dopt Opt_MultiParamTypeClasses dflags ||
isSingleton tys)
(instTypeErr (pprClassPred clas tys) head_one_type_msg)
- mapM_ check_one tys
+ mapM_ check_mono_type tys
+ -- For now, I only allow tau-types (not polytypes) in
+ -- the head of an instance decl.
+ -- E.g. instance C (forall a. a->a) is rejected
+ -- One could imagine generalising that, but I'm not sure
+ -- what all the consequences might be
+
where
head_type_synonym_msg = parens (
text "All instance types must be of the form (T t1 ... tn)" $$
text "Only one type can be given in an instance head." $$
text "Use -XMultiParamTypeClasses if you want to allow more.")
- -- For now, I only allow tau-types (not polytypes) in
- -- the head of an instance decl.
- -- E.g. instance C (forall a. a->a) is rejected
- -- One could imagine generalising that, but I'm not sure
- -- what all the consequences might be
- check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
- ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
-
instTypeErr pp_ty msg
= sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
nest 4 msg]