- case (getFunTy_maybe ty) of
- Just (arg,res) | (idType v `eqTy` arg) -> returnL(Just res)
- _ -> addErrL (mkAppMsg ty (idType v) e) `seqL` returnL Nothing
-
-lintCoreArg checkTyApp e ty a@(TyArg arg_ty)
- = -- TODO: Check that ty is well-kinded and has no unbound tyvars
- checkIfSpecDoneL (not (isPrimType arg_ty)) (mkSpecTyAppMsg a)
- `seqL`
- case (getForAllTy_maybe ty) of
- Just (tyvar,body) | (getTyVarKind tyvar == getTypeKind arg_ty) ->
- returnL(Just(instantiateTy [(tyvar,arg_ty)] body))
- _ -> addErrL (mkTyAppMsg ty arg_ty e) `seqL` returnL Nothing
+ case (getFunTyExpandingDicts_maybe False{-as above-} ty) of
+ Just (arg,res) | (var_ty `eqTy` arg) -> returnL(Just res)
+ _ -> addErrL (mkAppMsg ty var_ty e) `seqL` returnL Nothing
+ where
+ var_ty = idType v
+
+lintCoreArg e ty a@(TyArg arg_ty)
+ = -- ToDo: Check that ty is well-kinded and has no unbound tyvars
+ case (getForAllTyExpandingDicts_maybe ty) of
+ Nothing -> addErrL (mkTyAppMsg SLIT("Illegal") ty arg_ty e) `seqL` returnL Nothing
+
+ Just (tyvar,body) ->
+ let
+ tyvar_kind = tyVarKind tyvar
+ argty_kind = typeKind arg_ty
+ in
+ if argty_kind `hasMoreBoxityInfo` tyvar_kind
+ -- 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.
+ then
+ returnL(Just(instantiateTy [(tyvar,arg_ty)] body))
+ else
+ pprTrace "lintCoreArg:kinds:" (ppCat [ppr PprDebug tyvar_kind, ppr PprDebug argty_kind]) $
+ addErrL (mkTyAppMsg SLIT("Kinds not right in") ty arg_ty e) `seqL` returnL Nothing