import Literal ( literalType )
import DataCon ( dataConRepType, dataConTyCon, dataConWorkId )
import TysWiredIn ( tupleCon )
-import Var ( Var, Id, TyVar, idType, tyVarKind, mustHaveLocalBinding, setTyVarKind, setIdType )
+import Var ( Var, Id, TyVar, isCoVar, idType, tyVarKind,
+ mustHaveLocalBinding, setTyVarKind, setIdType )
import VarEnv ( lookupInScope )
import VarSet
import Name ( getSrcLoc )
mkLocMessage, debugTraceMsg )
import SrcLoc ( SrcLoc, noSrcLoc, mkSrcSpan )
import Type ( Type, tyVarsOfType, coreEqType,
- splitFunTy_maybe, mkTyVarTys,
+ splitFunTy_maybe,
splitForAllTy_maybe, splitTyConApp_maybe,
isUnLiftedType, typeKind, mkForAllTy, mkFunTy,
isUnboxedTupleType, isSubKind,
substTyWith, emptyTvSubst, extendTvInScope,
- TvSubst, TvSubstEnv, mkTvSubst, setTvSubstEnv, substTy,
- extendTvSubst, composeTvSubst, substTyVarBndr, isInScope,
- getTvSubstEnv, getTvInScope, mkTyVarTy )
-import Coercion ( Coercion, coercionKind )
-import TyCon ( isPrimTyCon )
+ TvSubst, substTy,
+ extendTvSubst, substTyVarBndr, isInScope,
+ getTvInScope )
+import Coercion ( coercionKind, coercionKindPredTy )
+import TyCon ( isPrimTyCon, isNewTyCon )
import BasicTypes ( RecFlag(..), Boxity(..), isNonRec )
import StaticFlags ( opt_PprStyle_Debug )
import DynFlags ( DynFlags, DynFlag(..), dopt )
lintCoreArg fun_ty arg =
-- Make sure function type matches argument
do { arg_ty <- lintCoreExpr arg
- ; let err = mkAppMsg fun_ty arg_ty arg
+ ; let err1 = mkAppMsg fun_ty arg_ty arg
+ err2 = mkNonFunAppMsg fun_ty arg_ty arg
; case splitFunTy_maybe fun_ty of
Just (arg,res) ->
- do { checkTys arg arg_ty err
+ do { checkTys arg arg_ty err1
; return res }
- _ -> addErrL err }
+ _ -> addErrL err2 }
\end{code}
\begin{code}
; checkKinds tyvar arg_ty
; return (substTyWith [tyvar] [arg_ty] body) }
-lintTyApps fun_ty [] = return fun_ty
-
-lintTyApps fun_ty (arg_ty : arg_tys) =
- do { fun_ty' <- lintTyApp fun_ty arg_ty
- ; lintTyApps fun_ty' arg_tys }
-
checkKinds tyvar arg_ty
-- Arg type might be boxed for a function with an uncommitted
-- tyvar; notably this is used so that we can give
-- error :: forall a:*. String -> a
-- and then apply it to both boxed and unboxed types.
- = checkL (argty_kind `isSubKind` tyvar_kind)
+ = checkL (arg_kind `isSubKind` tyvar_kind)
(mkKindErrMsg tyvar arg_ty)
where
tyvar_kind = tyVarKind tyvar
- argty_kind = typeKind arg_ty
+ arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
+ | otherwise = typeKind arg_ty
\end{code}
lit_ty = literalType lit
lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
+ | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
| Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
- = addLoc (CaseAlt alt) $ lintBinders args $ \ args ->
-
- do { addLoc (CasePat alt) $ do
- { -- Check the pattern
+ = addLoc (CaseAlt alt) $ do
+ { -- First instantiate the universally quantified
+ -- type variables of the data constructor
+ con_payload_ty <- lintCoreArgs (dataConRepType con) (map Type tycon_arg_tys)
+
+ -- And now bring the new binders into scope
+ ; lintBinders args $ \ args -> do
+ { addLoc (CasePat alt) $ do
+ { -- Check the pattern
-- Scrutinee type must be a tycon applicn; checked by caller
-- This code is remarkably compact considering what it does!
-- NB: args must be in scope here so that the lintCoreArgs line works.
-- NB: relies on existential type args coming *after* ordinary type args
- ; con_result_ty <-
- lintCoreArgs (dataConRepType con)
- (map Type tycon_arg_tys ++ varsToCoreExprs args)
+ ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
}
-- Check the RHS
- ; checkAltExpr rhs alt_ty }
+ ; checkAltExpr rhs alt_ty } }
| otherwise -- Scrut-ty is wrong shape
= addErrL (mkBadAltMsg scrut_ty alt)
Bag Message -> -- Error messages so far
(Maybe a, Bag Message) } -- Result and error messages (if any)
+{- Note [Type substitution]
+ ~~~~~~~~~~~~~~~~~~~~~~~~
+Why do we need a type substitution? Consider
+ /\(a:*). \(x:a). /\(a:*). id a x
+This is ill typed, because (renaming variables) it is really
+ /\(a:*). \(x:a). /\(b:*). id b x
+Hence, when checking an application, we can't naively compare x's type
+(at its binding site) with its expected type (at a use site). So we
+rename type binders as we go, maintaining a substitution.
+
+The same substitution also supports let-type, current expressed as
+ (/\(a:*). body) ty
+Here we substitute 'ty' for 'a' in 'body', on the fly.
+-}
+
instance Monad LintM where
return x = LintM (\ loc subst errs -> (Just x, errs))
fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
text "Scrutinee type:" <+> ppr scrut_ty,
text "Alternative:" <+> pprCoreAlt alt ]
+mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
+mkNewTyDataConAltMsg scrut_ty alt
+ = vcat [ text "Data alternative for newtype datacon",
+ text "Scrutinee type:" <+> ppr scrut_ty,
+ text "Alternative:" <+> pprCoreAlt alt ]
+
+
------------------------------------------------------
-- Other error messages
hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
hang (ptext SLIT("Arg:")) 4 (ppr arg)]
+mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
+mkNonFunAppMsg fun_ty arg_ty arg
+ = vcat [ptext SLIT("Non-function type in function position"),
+ hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
+ hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
+ hang (ptext SLIT("Arg:")) 4 (ppr arg)]
+
mkKindErrMsg :: TyVar -> Type -> Message
mkKindErrMsg tyvar arg_ty
= vcat [ptext SLIT("Kinds don't match in type application:"),
projects / ghc-hetmet.git / blobdiff