+newHole = newMutVar (error "Empty hole in typechecker")
+
+tcInfer :: (Expected ty -> TcM a) -> TcM (a,ty)
+tcInfer tc_infer
+ = do { hole <- newHole
+ ; res <- tc_infer (Infer hole)
+ ; res_ty <- readMutVar hole
+ ; return (res, res_ty) }
+
+readExpectedType :: Expected ty -> TcM ty
+readExpectedType (Infer hole) = readMutVar hole
+readExpectedType (Check ty) = returnM ty
+
+zapExpectedType :: Expected TcType -> Kind -> TcM TcTauType
+-- In the inference case, ensure we have a monotype
+-- (including an unboxed tuple)
+zapExpectedType (Infer hole) kind
+ = do { ty <- newTyFlexiVarTy kind ;
+ writeMutVar hole ty ;
+ return ty }
+
+zapExpectedType (Check ty) kind
+ | typeKind ty `isSubKind` kind = return ty
+ | otherwise = do { ty1 <- newTyFlexiVarTy kind
+ ; unifyTauTy ty1 ty
+ ; return ty }
+ -- The unify is to ensure that 'ty' has the desired kind
+ -- For example, in (case e of r -> b) we push an OpenTypeKind
+ -- type variable
+
+zapExpectedBranches :: MatchGroup id -> Expected TcRhoType -> TcM (Expected TcRhoType)
+-- If there is more than one branch in a case expression,
+-- and exp_ty is a 'hole', all branches must be types, not type schemes,
+-- otherwise the order in which we check them would affect the result.
+zapExpectedBranches (MatchGroup [match] _) exp_ty
+ = return exp_ty -- One branch
+zapExpectedBranches matches (Check ty)
+ = return (Check ty)
+zapExpectedBranches matches (Infer hole)
+ = do { -- Many branches, and inference mode,
+ -- so switch to checking mode with a monotype
+ ty <- newTyFlexiVarTy openTypeKind
+ ; writeMutVar hole ty
+ ; return (Check ty) }
+
+zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
+zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
+zapExpectedTo (Infer hole) ty2 = do { ty2' <- zonkTcType ty2; writeMutVar hole ty2' }
+ -- See Note [Zonk return type]
+
+instance Outputable ty => Outputable (Expected ty) where
+ ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
+ ppr (Infer hole) = ptext SLIT("Inferring type")
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection[Unify-fun]{@unifyFunTy@}
+%* *
+%************************************************************************
+
+@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
+creation of type variables.
+
+* subFunTy is used when we might be faced with a "hole" type variable,
+ in which case we should create two new holes.
+
+* unifyFunTy is used when we expect to encounter only "ordinary"
+ type variables, so we should create new ordinary type variables
+
+\begin{code}
+subFunTys :: MatchGroup name
+ -> Expected TcRhoType -- Fail if ty isn't a function type
+ -> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a)
+ -> TcM a
+
+subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside
+ = -- This is the interesting case
+ ASSERT( null null_matches )
+ do { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match)
+ ; res_hole <- newHole
+
+ -- Do the business
+ ; res <- thing_inside (map Infer pat_holes) (Infer res_hole)
+
+ -- Extract the answers
+ ; arg_tys <- mapM readMutVar pat_holes
+ ; res_ty <- readMutVar res_hole
+
+ -- Write the answer into the incoming hole
+ ; writeMutVar hole (mkFunTys arg_tys res_ty)
+
+ -- And return the answer
+ ; return res }
+
+subFunTys (MatchGroup (match:matches) _) (Check ty) thing_inside
+ = ASSERT( all ((== length (hsLMatchPats match)) . length . hsLMatchPats) matches )
+ -- Assertion just checks that all the matches have the same number of pats
+ do { (pat_tys, res_ty) <- unifyFunTys (length (hsLMatchPats match)) ty
+ ; thing_inside (map Check pat_tys) (Check res_ty) }
+
+unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
+-- Fail if ty isn't a function type, otherwise return arg and result types
+-- The result types are guaranteed wobbly if the argument is wobbly
+--
+-- Does not allocate unnecessary meta variables: if the input already is
+-- a function, we just take it apart. Not only is this efficient, it's important
+-- for (a) higher rank: the argument might be of form
+-- (forall a. ty) -> other
+-- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
+-- blow up with the meta var meets the forall
+--
+-- (b) GADTs: if the argument is not wobbly we do not want the result to be
+
+unifyFunTys arity ty = unify_fun_ty True arity ty
+
+unify_fun_ty use_refinement arity ty
+ | arity == 0
+ = do { res_ty <- wobblify use_refinement ty
+ ; return ([], ty) }
+
+unify_fun_ty use_refinement arity (NoteTy _ ty)
+ = unify_fun_ty use_refinement arity ty
+
+unify_fun_ty use_refinement arity ty@(TyVarTy tv)
+ = do { details <- condLookupTcTyVar use_refinement tv
+ ; case details of
+ IndirectTv use' ty' -> unify_fun_ty use' arity ty'
+ other -> unify_fun_help arity ty
+ }
+
+unify_fun_ty use_refinement arity ty
+ = case tcSplitFunTy_maybe ty of
+ Just (arg,res) -> do { arg' <- wobblify use_refinement arg
+ ; (args', res') <- unify_fun_ty use_refinement (arity-1) res
+ ; return (arg':args', res') }
+
+ Nothing -> unify_fun_help arity ty
+ -- Usually an error, but ty could be (a Int Bool), which can match
+
+unify_fun_help :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
+unify_fun_help arity ty
+ = do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind)
+ ; res <- newTyFlexiVarTy openTypeKind
+ ; unifyTauTy ty (mkFunTys args res)
+ ; return (args, res) }
+\end{code}
+
+\begin{code}
+----------------------
+zapToTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
+ -> Expected TcSigmaType -- Expected type (T a b c)
+ -> TcM [TcType] -- Element types, a b c
+ -- Insists that the Expected type is not a forall-type
+
+zapToTyConApp tc (Check ty)
+ = unifyTyConApp tc ty -- NB: fails for a forall-type
+zapToTyConApp tc (Infer hole)
+ = do { (tc_app, elt_tys) <- newTyConApp tc
+ ; writeMutVar hole tc_app
+ ; return elt_tys }
+
+zapToListTy :: Expected TcType -> TcM TcType -- Special case for lists
+zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty
+ ; return elt_ty }
+
+----------------------
+unifyTyConApp :: TyCon -> TcType -> TcM [TcType]
+unifyTyConApp tc ty = unify_tc_app True tc ty
+ -- Add a boolean flag to remember whether to use
+ -- the type refinement or not
+
+unifyListTy :: TcType -> TcM TcType -- Special case for lists
+unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty
+ ; return elt_ty }
+
+----------
+unify_tc_app use_refinement tc (NoteTy _ ty)
+ = unify_tc_app use_refinement tc ty
+
+unify_tc_app use_refinement tc ty@(TyVarTy tyvar)
+ = do { details <- condLookupTcTyVar use_refinement tyvar
+ ; case details of
+ IndirectTv use' ty' -> unify_tc_app use' tc ty'
+ other -> unify_tc_app_help tc ty
+ }
+
+unify_tc_app use_refinement tc ty
+ | Just (tycon, arg_tys) <- tcSplitTyConApp_maybe ty,
+ tycon == tc
+ = ASSERT( tyConArity tycon == length arg_tys ) -- ty::*
+ mapM (wobblify use_refinement) arg_tys
+
+unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty
+
+----------
+unify_tc_app_help tc ty -- Revert to ordinary unification
+ = do { (tc_app, arg_tys) <- newTyConApp tc
+ ; if not (isTauTy ty) then -- Can happen if we call zapToTyConApp tc (forall a. ty)
+ unifyMisMatch ty tc_app
+ else do
+ { unifyTauTy ty tc_app
+ ; returnM arg_tys } }
+
+
+----------------------
+unifyAppTy :: TcType -- Expected type function: m
+ -> TcType -- Type to split: m a
+ -> TcM TcType -- Type arg: a
+unifyAppTy tc ty = unify_app_ty True tc ty
+
+unify_app_ty use tc (NoteTy _ ty) = unify_app_ty use tc ty
+
+unify_app_ty use tc ty@(TyVarTy tyvar)
+ = do { details <- condLookupTcTyVar use tyvar
+ ; case details of
+ IndirectTv use' ty' -> unify_app_ty use' tc ty'
+ other -> unify_app_ty_help tc ty
+ }
+
+unify_app_ty use tc ty
+ | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
+ = do { unifyTauTy tc fun_ty
+ ; wobblify use arg_ty }
+
+ | otherwise = unify_app_ty_help tc ty
+
+unify_app_ty_help tc ty -- Revert to ordinary unification
+ = do { arg_ty <- newTyFlexiVarTy (kindFunResult (typeKind tc))
+ ; unifyTauTy (mkAppTy tc arg_ty) ty
+ ; return arg_ty }
+
+
+----------------------
+wobblify :: Bool -- True <=> don't wobblify
+ -> TcTauType
+ -> TcM TcTauType
+-- Return a wobbly type. At the moment we do that by
+-- allocating a fresh meta type variable.
+wobblify True ty = return ty
+wobblify False ty = do { uniq <- newUnique
+ ; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w"))
+ (typeKind ty)
+ (Indirect ty)
+ ; return (mkTyVarTy tv) }
+
+----------------------
+newTyConApp :: TyCon -> TcM (TcTauType, [TcTauType])
+newTyConApp tc = do { (tvs, args, _) <- tcInstTyVars (tyConTyVars tc)
+ ; return (mkTyConApp tc args, args) }
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Subsumption}
+%* *
+%************************************************************************
+
+All the tcSub calls have the form
+
+ tcSub expected_ty offered_ty
+which checks
+ offered_ty <= expected_ty
+
+That is, that a value of type offered_ty is acceptable in
+a place expecting a value of type expected_ty.
+
+It returns a coercion function
+ co_fn :: offered_ty -> expected_ty
+which takes an HsExpr of type offered_ty into one of type
+expected_ty.
+
+\begin{code}
+-----------------------
+-- tcSubExp is used for expressions
+tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
+
+tcSubExp (Infer hole) offered_ty
+ = do { offered' <- zonkTcType offered_ty
+ -- Note [Zonk return type]
+ -- zonk to take advantage of the current GADT type refinement.
+ -- If we don't we get spurious "existential type variable escapes":
+ -- case (x::Maybe a) of
+ -- Just b (y::b) -> y
+ -- We need the refinement [b->a] to be applied to the result type
+ ; writeMutVar hole offered'
+ ; return idCoercion }
+
+tcSubExp (Check expected_ty) offered_ty
+ = tcSub expected_ty offered_ty
+
+-----------------------
+-- tcSubPat is used for patterns
+tcSubPat :: TcSigmaType -- Pattern type signature
+ -> Expected TcSigmaType -- Type from context
+ -> TcM ()
+-- In patterns we insist on an exact match; hence no CoFn returned
+-- See Note [Pattern coercions] in TcPat
+-- However, we can't call unify directly, because both types might be
+-- polymorphic; hence the call to tcSub, followed by a check for
+-- the identity coercion
+
+tcSubPat sig_ty (Infer hole)
+ = do { sig_ty' <- zonkTcType sig_ty
+ ; writeMutVar hole sig_ty' -- See notes with tcSubExp above
+ ; return () }
+
+tcSubPat sig_ty (Check exp_ty)
+ = do { co_fn <- tcSub sig_ty exp_ty
+
+ ; if isIdCoercion co_fn then
+ return ()
+ else
+ unifyMisMatch sig_ty exp_ty }
+\end{code}
+
+
+
+%************************************************************************
+%* *
+ tcSub: main subsumption-check code
+%* *
+%************************************************************************
+
+No holes expected now. Add some error-check context info.
+
+\begin{code}
+-----------------
+tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
+ -- tcSub exp act checks that
+ -- act <= exp
+tcSub expected_ty actual_ty
+ = traceTc (text "tcSub" <+> details) `thenM_`
+ addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
+ (tc_sub expected_ty expected_ty actual_ty actual_ty)
+ where
+ details = vcat [text "Expected:" <+> ppr expected_ty,
+ text "Actual: " <+> ppr actual_ty]
+
+-----------------
+tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
+ -> TcSigmaType -- ..and after
+ -> TcSigmaType -- actual_ty, before
+ -> TcSigmaType -- ..and after
+ -> TcM ExprCoFn
+
+-----------------------------------
+-- Expand synonyms
+tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
+tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
+
+-----------------------------------
+-- Generalisation case
+-- actual_ty: d:Eq b => b->b
+-- expected_ty: forall a. Ord a => a->a
+-- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
+
+-- It is essential to do this *before* the specialisation case
+-- Example: f :: (Eq a => a->a) -> ...
+-- g :: Ord b => b->b
+-- Consider f g !
+
+tc_sub exp_sty expected_ty act_sty actual_ty
+ | isSigmaTy expected_ty
+ = tcGen expected_ty (tyVarsOfType actual_ty) (
+ -- It's really important to check for escape wrt the free vars of
+ -- both expected_ty *and* actual_ty
+ \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
+ ) `thenM` \ (gen_fn, co_fn) ->
+ returnM (gen_fn <.> co_fn)
+
+-----------------------------------
+-- Specialisation case:
+-- actual_ty: forall a. Ord a => a->a
+-- expected_ty: Int -> Int
+-- co_fn e = e Int dOrdInt
+
+tc_sub exp_sty expected_ty act_sty actual_ty
+ | isSigmaTy actual_ty
+ = tcInstCall InstSigOrigin actual_ty `thenM` \ (inst_fn, _, body_ty) ->
+ tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
+ returnM (co_fn <.> inst_fn)
+
+-----------------------------------
+-- Function case
+
+tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
+ = tcSub_fun exp_arg exp_res act_arg act_res
+
+-----------------------------------
+-- Type variable meets function: imitate
+--
+-- NB 1: we can't just unify the type variable with the type
+-- because the type might not be a tau-type, and we aren't
+-- allowed to instantiate an ordinary type variable with
+-- a sigma-type
+--
+-- NB 2: can we short-cut to an error case?
+-- when the arg/res is not a tau-type?
+-- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
+-- then x = (f,f)
+-- is perfectly fine, because we can instantiate f's type to a monotype
+--
+-- However, we get can get jolly unhelpful error messages.
+-- e.g. foo = id runST
+--
+-- Inferred type is less polymorphic than expected
+-- Quantified type variable `s' escapes
+-- Expected type: ST s a -> t
+-- Inferred type: (forall s1. ST s1 a) -> a
+-- In the first argument of `id', namely `runST'
+-- In a right-hand side of function `foo': id runST
+--
+-- I'm not quite sure what to do about this!
+
+tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty
+ = do { ([act_arg], act_res) <- unifyFunTys 1 act_ty
+ ; tcSub_fun exp_arg exp_res act_arg act_res }
+
+tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res)
+ = do { ([exp_arg], exp_res) <- unifyFunTys 1 exp_ty
+ ; tcSub_fun exp_arg exp_res act_arg act_res }
+
+-----------------------------------
+-- Unification case
+-- If none of the above match, we revert to the plain unifier
+tc_sub exp_sty expected_ty act_sty actual_ty
+ = uTys True exp_sty expected_ty True act_sty actual_ty `thenM_`
+ returnM idCoercion
+\end{code}
+
+\begin{code}
+tcSub_fun exp_arg exp_res act_arg act_res
+ = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
+ tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
+ newUnique `thenM` \ uniq ->
+ let
+ -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
+ -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
+ -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
+ arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
+ coercion | isIdCoercion co_fn_arg,
+ isIdCoercion co_fn_res = idCoercion
+ | otherwise = mkCoercion co_fn
+
+ co_fn e = DictLam [arg_id]
+ (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
+ -- Slight hack; using a "DictLam" to get an ordinary simple lambda
+ -- HsVar arg_id :: HsExpr exp_arg
+ -- co_fn_arg $it :: HsExpr act_arg
+ -- HsApp e $it :: HsExpr act_res
+ -- co_fn_res $it :: HsExpr exp_res
+ in
+ returnM coercion