+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) }