+subFunTys :: SDoc -- Somthing like "The function f has 3 arguments"
+ -- or "The abstraction (\x.e) takes 1 argument"
+ -> Arity -- Expected # of args
+ -> BoxyRhoType -- res_ty
+ -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
+ -> TcM (ExprCoFn, a)
+-- Attempt to decompse res_ty to have enough top-level arrows to
+-- match the number of patterns in the match group
+--
+-- If (subFunTys n_args res_ty thing_inside) = (co_fn, res)
+-- and the inner call to thing_inside passes args: [a1,...,an], b
+-- then co_fn :: (a1 -> ... -> an -> b) -> res_ty
+--
+-- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType
+
+
+{- Error messages from subFunTys
+
+ The abstraction `\Just 1 -> ...' has two arguments
+ but its type `Maybe a -> a' has only one
+
+ The equation(s) for `f' have two arguments
+ but its type `Maybe a -> a' has only one
+
+ The section `(f 3)' requires 'f' to take two arguments
+ but its type `Int -> Int' has only one
+
+ The function 'f' is applied to two arguments
+ but its type `Int -> Int' has only one
+-}
+
+
+subFunTys error_herald n_pats res_ty thing_inside
+ = loop n_pats [] res_ty
+ where
+ -- In 'loop', the parameter 'arg_tys' accumulates
+ -- the arg types so far, in *reverse order*
+ loop n args_so_far res_ty
+ | Just res_ty' <- tcView res_ty = loop n args_so_far res_ty'
+
+ loop n args_so_far res_ty
+ | isSigmaTy res_ty -- Do this before checking n==0, because we
+ -- guarantee to return a BoxyRhoType, not a BoxySigmaType
+ = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ res_ty' ->
+ loop n args_so_far res_ty'
+ ; return (gen_fn <.> co_fn, res) }
+
+ loop 0 args_so_far res_ty
+ = do { res <- thing_inside (reverse args_so_far) res_ty
+ ; return (idCoercion, res) }
+
+ loop n args_so_far (FunTy arg_ty res_ty)
+ = do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty
+ ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
+ ; return (co_fn', res) }
+
+ -- res_ty might have a type variable at the head, such as (a b c),
+ -- in which case we must fill in with (->). Simplest thing to do
+ -- is to use boxyUnify, but we catch failure and generate our own
+ -- error message on failure
+ loop n args_so_far res_ty@(AppTy _ _)
+ = do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
+ ; (_, mb_unit) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty')
+ ; if isNothing mb_unit then bale_out args_so_far res_ty
+ else loop n args_so_far (FunTy arg_ty' res_ty') }
+
+ loop n args_so_far (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop n args_so_far ty
+ Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
+ ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty
+ ; return (idCoercion, res) } }
+ where
+ mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
+ kinds = openTypeKind : take n (repeat argTypeKind)
+ -- Note argTypeKind: the args can have an unboxed type,
+ -- but not an unboxed tuple.
+
+ loop n args_so_far res_ty = bale_out args_so_far res_ty
+
+ bale_out args_so_far res_ty
+ = do { env0 <- tcInitTidyEnv
+ ; res_ty' <- zonkTcType res_ty
+ ; let (env1, res_ty'') = tidyOpenType env0 res_ty'
+ ; failWithTcM (env1, mk_msg res_ty'' (length args_so_far)) }
+
+ mk_msg res_ty n_actual
+ = error_herald <> comma $$
+ sep [ptext SLIT("but its type") <+> quotes (pprType res_ty),
+ if n_actual == 0 then ptext SLIT("has none")
+ else ptext SLIT("has only") <+> speakN n_actual]
+\end{code}
+
+\begin{code}
+----------------------
+boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
+ -> BoxyRhoType -- Expected type (T a b c)
+ -> TcM [BoxySigmaType] -- Element types, a b c
+ -- It's used for wired-in tycons, so we call checkWiredInTyCOn
+ -- Precondition: never called with FunTyCon
+ -- Precondition: input type :: *
+
+boxySplitTyConApp tc orig_ty
+ = do { checkWiredInTyCon tc
+ ; loop (tyConArity tc) [] orig_ty }
+ where
+ loop n_req args_so_far ty
+ | Just ty' <- tcView ty = loop n_req args_so_far ty'
+
+ loop n_req args_so_far (TyConApp tycon args)
+ | tc == tycon
+ = ASSERT( n_req == length args) -- ty::*
+ return (args ++ args_so_far)
+
+ loop n_req args_so_far (AppTy fun arg)
+ = loop (n_req - 1) (arg:args_so_far) fun
+
+ loop n_req args_so_far (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop n_req args_so_far ty
+ Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
+ ; return (arg_tys ++ args_so_far) }
+ }
+ where
+ mk_res_ty arg_tys' = mkTyConApp tc arg_tys'
+ arg_kinds = map tyVarKind (take n_req (tyConTyVars tc))
+
+ loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty
+
+----------------------
+boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType -- Special case for lists
+boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty
+ ; return elt_ty }
+
+
+----------------------
+boxySplitAppTy :: BoxyRhoType -- Type to split: m a
+ -> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a
+-- Assumes (m: * -> k), where k is the kind of the incoming type
+-- If the incoming type is boxy, then so are the result types; and vice versa
+
+boxySplitAppTy orig_ty
+ = loop orig_ty
+ where
+ loop ty
+ | Just ty' <- tcView ty = loop ty'
+
+ loop ty
+ | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
+ = return (fun_ty, arg_ty)
+
+ loop (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop ty
+ Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty
+ ; return (fun_ty, arg_ty) } }
+ where
+ mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
+ tv_kind = tyVarKind tv
+ kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
+ -- m :: * -> k
+ liftedTypeKind] -- arg type :: *
+ -- The defaultKind is a bit smelly. If you remove it,
+ -- try compiling f x = do { x }
+ -- and you'll get a kind mis-match. It smells, but
+ -- not enough to lose sleep over.
+
+ loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
+
+------------------
+boxySplitFailure actual_ty expected_ty
+ = unifyMisMatch False False actual_ty expected_ty
+ -- "outer" is False, so we don't pop the context
+ -- which is what we want since we have not pushed one!
+\end{code}
+
+
+--------------------------------
+-- withBoxes: the key utility function
+--------------------------------
+
+\begin{code}
+withMetaTvs :: TcTyVar -- An unfilled-in, non-skolem, meta type variable
+ -> [Kind] -- Make fresh boxes (with the same BoxTv/TauTv setting as tv)
+ -> ([BoxySigmaType] -> BoxySigmaType)
+ -- Constructs the type to assign
+ -- to the original var
+ -> TcM [BoxySigmaType] -- Return the fresh boxes
+
+-- It's entirely possible for the [kind] to be empty.
+-- For example, when pattern-matching on True,
+-- we call boxySplitTyConApp passing a boolTyCon
+
+-- Invariant: tv is still Flexi
+
+withMetaTvs tv kinds mk_res_ty
+ | isBoxyTyVar tv
+ = do { box_tvs <- mapM (newMetaTyVar BoxTv) kinds
+ ; let box_tys = mkTyVarTys box_tvs
+ ; writeMetaTyVar tv (mk_res_ty box_tys)
+ ; return box_tys }
+
+ | otherwise -- Non-boxy meta type variable
+ = do { tau_tys <- mapM newFlexiTyVarTy kinds
+ ; writeMetaTyVar tv (mk_res_ty tau_tys) -- Write it *first*
+ -- Sure to be a tau-type
+ ; return tau_tys }
+
+withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
+-- Allocate a *boxy* tyvar
+withBox kind thing_inside
+ = do { box_tv <- newMetaTyVar BoxTv kind
+ ; res <- thing_inside (mkTyVarTy box_tv)
+ ; ty <- readFilledBox box_tv
+ ; return (res, ty) }