-- -- Copyright (C) 2005 Stefan Wehr - http://www.stefanwehr.de -- -- This program is free software; you can redistribute it and/or -- modify it under the terms of the GNU General Public License as -- published by the Free Software Foundation; either version 2 of -- the License, or (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -- General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program; if not, write to the Free Software -- Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -- 02111-1307, USA. -- module Phrac.TypeInference ( tiMain, emptyAssumps, dumpTypeInference ) where import Control.Monad.State import Control.Monad.Error import qualified Data.Set as Set import List (partition, intersperse, filter,nub) import qualified Data.Generics as Gen import Maybe ( fromJust ) import qualified Phrac.Map as Map import qualified Phrac.Builtins as Builtins import Phrac.UniqIdents ( builtinTypeId ) import Phrac.AbstractSyntax import Phrac.Substitution import Phrac.Error import Phrac.Pretty import Phrac.Symtab import Phrac.Unification hiding (unify) import Phrac.Entailment ( entail, split, splitToplevel, reduce ) import Phrac.Kinds import Phrac.DependAnalysis import Phrac.Overloading type Assumps = Map.Map ValId TypeScheme emptyAssumps = Map.empty find :: ValId -> Assumps -> TypeScheme find i as = case Map.lookup i as of Just t -> t Nothing -> panic ("variable `" ++ showPpr i ++ "' not found in assumptions: " ++ dumpAssumps as) singleton :: ValId -> TypeScheme -> Assumps singleton v sc = add v sc emptyAssumps add :: ValId -> TypeScheme -> Assumps -> Assumps add i t as = Map.insert i t as merge :: Assumps -> Assumps -> Assumps merge as as' = if not (Set.null $ Map.keysSet as `Set.intersection` Map.keysSet as') then panic ("cannot merge assumptions, they have at most one key " ++ "in common:\n\nAssumptions 1:\n" ++ dumpAssumps as ++ "\n\nAssumptions 2:\n" ++ dumpAssumps as') else Map.union as as' buildAssumps :: [ValId] -> [TypeScheme] -> Assumps buildAssumps is ts = Map.fromList (zip is ts) dumpAssumps :: Assumps -> String dumpAssumps as = "{Assumptions: " ++ showCommaListed (map (\ (k,v) -> ppr k <+> text "=" <+> ppr v) (Map.assocs as)) ++ "}" tiDebug :: Location -> String -> ([ClassConstraint], [EqConstraint]) -> Type -> TI () tiDebug loc str constrs t = do s <- gets ti_subst let (cs, es) = applySubst s constrs t' = applySubst s t msg = "TypeInference, " ++ str ++ ": " ++ dumpClassConstraints cs ++ ", " ++ dumpEqConstraints es ++ ", type = " ++ showPpr t debug_ loc msg data TIState = TIState { ti_subst :: TypeSubst } emptyTIState = TIState { ti_subst = nullSubst } type TI = StateT TIState ST liftST :: ST a -> TI a liftST x = lift x runTI :: TI a -> ST a runTI ti = evalStateT ti emptyTIState unify :: [EqConstraint] -> Type -> Type -> TI [EqConstraint] unify eqc t1 t2 = do s <- gets ti_subst let eq = (applySubst s t1) :=: (applySubst s t2) eqs = map toTypeEq (applySubst s eqc) ures <- liftST $ runUnify [] (eq : eqs) case ures of Left err -> phasefail err Right (eqc', s') -> let newSubst = s' `composeSubst` s in do modify (\state -> state { ti_subst = newSubst }) return eqc' where toTypeEq (EqConstraint l r) = TyAssoc l :=: r type Infer e t = Assumps -> e -> TI ([Constraint], t, e) tiPats :: [Pat] -> TI ([Constraint], Assumps, [Type]) tiPats ps = do l <- mapM tiPat ps let (pss, ass, ts) = unzip3 l return (concat pss, foldr merge emptyAssumps ass, ts) tiPat :: Pat -> TI ([Constraint], Assumps, Type) tiPat PWildcard = do alpha <- lift $ freshTypeVar KindStar return ([], emptyAssumps, alpha) tiPat (PVar i) = do alpha <- lift $ freshTypeVar KindStar return ([], singleton i (toScheme alpha), alpha) tiPat (PAs i p) = do (ps, as, t) <- tiPat p return (ps, add i (toScheme t) as, t) tiPat (PCon i ps) = do (ps, as, ts) <- tiPats ps alpha <- lift $ freshTypeVar KindStar sc <- liftST $ typeOfDataConstructor i (qs, t) <- freshInst sc ecs <- unify [] t (tyFuns ts alpha) return (map EC ecs ++ ps ++ qs, as, alpha) tiExpr :: Infer Exp Type tiExpr as (Var i) = do let sc = find i as (ps, t) <- freshInst sc b <- lift $ isMethod i let cs = classConstraints ps e = if null cs then (Var i) else if b then foldl App (mp i (head cs)) (map ph (tail cs)) else foldl App (Var i) (map ph cs) return (ps, t, e) where ph cc = Overloading $ Placeholder cc mp i (ClassConstraint cid ts) = Overloading $ MethodPlaceholder cid i ts tiExpr as e@(Const (Number _)) = return $ ([], TyConstruct intTypeId, e) tiExpr as e@(Const (Character _)) = return $ ([], TyConstruct charTypeId, e) tiExpr as (Prim op es) = do l <- mapM (tiExpr as) es let (pss, operandTypes, es') = unzip3 l alpha <- liftST $ freshTypeVar KindStar let opTy = typeOfPrimOp op resTy = tyFuns operandTypes alpha qs <- unify [] opTy resTy return (map EC qs ++ concat pss, alpha, Prim op es') tiExpr as (Con di es) = do sc <- liftST $ typeOfDataConstructor di (ps, t) <- freshInst sc alpha <- liftST $ freshTypeVar KindStar l <- mapM (tiExpr as) es let (pss, operandTypes, es') = unzip3 l t' = tyFuns operandTypes alpha qs <- unify [] t t' return (ps ++ map EC qs ++ concat pss, alpha, Con di es') tiExpr as (App e1 e2) = do (ps1, tau1, e1') <- tiExpr as e1 (ps2, tau2, e2') <- tiExpr as e2 let (theta1, u1) = splitConstraints ps1 (theta2, u2) = splitConstraints ps2 alpha <- liftST $ freshTypeVar KindStar u <- unify (u1 ++ u2) tau1 (tau2 `tyFun` alpha) return (mergeConstraints (theta1 ++ theta2) u, alpha, App e1' e2') -- \x1 .. xN -> e is rewritten as \x1 -> .. \xN -> e tiExpr as (Lam [] e) = tiExpr as e tiExpr as (Lam (x:xs) e) = do (ps, as', t) <- tiPat x (qs, tau, e') <- tiExpr (as' `merge` as) (Lam xs e) return (ps ++ qs, t `tyFun` tau, Lam [x] e') tiExpr as (If e1 e2 e3) = do (ps1, t1, e1') <- tiExpr as e1 qs1 <- unify [] t1 boolType alpha <- liftST $ freshTypeVar KindStar (ps2, t2, e2') <- tiExpr as e2 (ps3, t3, e3') <- tiExpr as e3 qs2 <- unify [] t2 alpha qs3 <- unify [] t3 alpha return (ps1 ++ ps2 ++ ps3 ++ (map EC $ qs1 ++ qs2 ++ qs3), alpha, If e1' e2' e3') tiExpr as (Letrec binds e) = do (ps, as', binds') <- tiBindGroup NestedLevel as binds (qs, t, e') <- tiExpr (as' `merge` as) e return (ps ++ qs, t, Letrec binds' e') tiExpr as (Case e alts) = do (ps, t, e') <- tiExpr as e l <- mapM (\ (Alt pat _) -> tiPat pat) alts let (pss, ass, ts) = unzip3 l qss <- mapM (unify [] t) ts let es = map alt_exp alts l' <- mapM (\ (as', e') -> tiExpr (as' `merge` as) e') (zip ass es) let (rss, resTys, es') = unzip3 l' alpha <- liftST $ freshTypeVar KindStar qss' <- mapM (unify [] alpha) resTys let alts' = map (\ (a,e) -> a { alt_exp = e }) (zip alts es') return (ps ++ concat (pss ++ rss) ++ map EC (concat (qss ++ qss')), alpha, Case e' alts') -- tiBind is tiAlt in THIH tiBind :: Infer Bind Type tiBind as (pats, e) = do (ps, as', ts) <- tiPats pats (qs, t, e') <- tiExpr (as' `merge` as) e let resTy = tyFuns ts t return (ps ++ qs, resTy, (pats, e')) type Expl = (ValId, TypeScheme, Bind) -- returns the deferred constraints tiExpl :: Assumps -> Expl -> TI ([Constraint], Expl) tiExpl as (i, sc@(TypeScheme _ (QualifiedType qs _)), bind) = do -- we check for ambiguity first because ambiguous signatures may -- not pass the subsumption check, although they look like they should checkForAmbiguity (i, sc) display ("typing explicitly typed binding " ++ showPpr' i) (ps, t, bind') <- tiBind as bind -- infered type s <- gets ti_subst let t' = applySubst s t ps' = applySubst s ps as' = applySubst s as fs = freeTypeVars as' gs = (freeTypeVars ps' `Set.union` freeTypeVars t') `Set.difference` fs (ds, ps'') <- liftST $ split (Set.toList fs) (Set.toList gs) ps' sc' <- generalize i (Set.toList gs) ps'' t' debug ("type infered for " ++ showPpr' i ++ ": " ++ showPpr sc' ++ ", now checking for subsumption") msubst <- subsumes sc' sc case msubst of Nothing -> phasefail ("type error while checking explicitly typed binding " ++ showPpr' i ++ "\n infered signature: " ++ showPpr sc' ++ "\n user-supplied signature: " ++ showPpr sc) Just (s1,s2) -> do -- Overloading resolution is a bit tricky here... -- We must first replace the type variables in the user-supplied -- signature with the type constructors used during subsumption -- (s1 is used for that) let cs = classConstraints (applySubst s1 qs) -- Then we must replace the type variables in the place holder -- with the same type constructors (use (s2 . s) for that) let bind'' = Gen.everywhere (Gen.mkT (transPH (s2 `composeSubst` s))) bind' resBind <- tiResolveOverloading i [] cs bind'' debug ("Finished typing explicitly typed binding " ++ showPpr' i ++ " deferred constraints: " ++ showCommaListed ds ++ "\n\n" ++ showTypeSig (i,sc) ++ "\n\n") return (ds, (i, sc, resBind)) where transPH :: TypeSubst -> Overloading -> Overloading transPH s (Placeholder c) = Placeholder (applySubst s c) transPH s (MethodPlaceholder cid vid ts) = MethodPlaceholder cid vid (applySubst s ts) transPH _ o = o type Impl = (ValId, Bind) data Level = TopLevel | NestedLevel deriving (Show,Eq) -- returns the deferred constraints and the types for the bindings tiImpls :: Level -> Infer [Impl] Assumps tiImpls level as bs = do let is = map fst bs display ("typing implicitly typed bindings " ++ showCommaListed is) -- type for every bindind ts <- liftST $ mapM (\_ -> freshTypeVar KindStar) bs let scs = map toScheme ts as' = as `merge` buildAssumps is scs l <- mapM (tiBind as') (map snd bs) let (pss, types, bs') = unzip3 l pss' <- mapM (uncurry $ unify []) (zip ts types) let ps = concat pss ++ (map EC $ concat pss') s <- gets ti_subst let ps' = applySubst s ps ts' = applySubst s ts as' = applySubst s as fs = freeTypeVars as' vss = map freeTypeVars ts' gs = Set.unions vss `Set.difference` fs debug ("monotypes for implicitly type bindings: " ++ showCommaListed (map (\ (i, t) -> ppr i <+> text " :: " <+> ppr t) (zip is ts')) ++ ", constraints: " ++ showCommaListed ps') let mySplit = if level == TopLevel then splitToplevel else split (ds, rs) <- liftST $ mySplit (Set.toList fs) (Set.toList $ foldr1 Set.intersection vss) ps' (constrs, scs', bs'') <- if restricted bs then do let gs' = gs `Set.difference` (freeTypeVars rs) scs'' <- mapM (\ (i,t) -> generalize i (Set.toList gs') [] t) (zip is ts') bs''' <- mapM (\ (i,b) -> tiResolveOverloading i is [] b) (zip is bs') debug ("The monomorphism restriction applies") return (ds ++ rs, scs'', bs''') else do scs'' <- mapM (\ (i,t) -> generalize i (Set.toList gs) rs t) (zip is ts') bs''' <- mapM (\ (i,b) -> tiResolveOverloading i is (classConstraints rs) b) (zip is bs') debug ("The monomorphism restriction does not apply") return (ds, scs'', bs''') let resAssumps = buildAssumps is scs' resImpls = zip is bs'' debug ("finished typing implicitly typed bindings, deferred " ++ "constraints: " ++ showCommaListed constrs) return (constrs, resAssumps, resImpls) where restricted :: [Impl] -> Bool restricted bs = let simple (i, b) = null (fst b) in any simple bs splitImpls :: [Impl] -> [[Impl]] splitImpls bs = getBindGroups bs fst getDeps where getDeps (id, (args, e)) = let is = map fst bs in filter (`elem` is) (freeVars e) freeVars e = -- variable names are unique, so we can just collect all variables Gen.everything (++) ([] `Gen.mkQ` collectVar) e collectVar :: Exp -> [ValId] collectVar (Var id) = [id] collectVar _ = [] tiImplsSeq :: Level -> Infer [[Impl]] Assumps tiImplsSeq _ as [] = return ([], emptyAssumps, []) tiImplsSeq level as (bs:bss) = do (ps, as', bs') <- tiImpls level as bs (qs, as'', bss') <- tiImplsSeq level (as' `merge` as) bss return (ps ++ qs, as'' `merge` as', bs' : bss') tiBindGroup :: Level -> Infer [ValBind] Assumps tiBindGroup level as binds = do let ids = map vbind_name binds debug ("typing binding group " ++ showCommaListed ids ++ " under the assumption " ++ dumpAssumps as) let (as', expls, impls) = collect emptyAssumps binds debug ("assumptions resulting from explicitly typed bindings: " ++ dumpAssumps as') (ps, as'', impls') <- tiImplsSeq level (as' `merge` as) (splitImpls impls) debug ("assumptions obtained by typing the implicitly typed bindings: " ++ dumpAssumps as'' ++ ", constraints: " ++ showCommaListed ps) l <- mapM (tiExpl (as'' `merge` as' `merge` as)) expls let (qss, expls') = unzip l let resConstrs = concat qss ++ ps resAssumps = as'' `merge` as' resBinds = reconstructValBinds binds impls' expls' debug ("finished typing binding group " ++ showCommaListed ids ++ ", resulting assumptions: " ++ dumpAssumps resAssumps ++ ", resulting constraints: " ++ showCommaListed resConstrs) return (resConstrs, resAssumps, resBinds) where collect as [] = (as, [], []) collect as (ValBind id Nothing params e _ : rest) = let (as', expls, impls) = collect as rest in (as', expls, (id, (params, e)) : impls) collect as (ValBind id (Just t) params e _ : rest) = let (as', expls, impls) = collect as rest in (add id t as', (id, t, (params, e)) : expls, impls) reconstructValBinds :: [ValBind] -> [[Impl]] -> [Expl] -> [ValBind] reconstructValBinds origBinds impls expls = let bs = concat impls ++ (map (\ (i, sc, b) -> (i, b)) expls) replExp vb = let (pats, e) = fromJust (lookup (vbind_name vb) bs) in vb { vbind_exp = e, vbind_pats = pats } in map replExp origBinds tiMain :: Assumps -> Program -> ST (Assumps, Program) tiMain initAs prog@(Program _ classes instances valBinds) = do (ps, as, valBinds', instances') <- runTI $ ti classes instances valBinds if not (null ps) then phasefail ("deferred constraints left after type inference:\n" ++ dumpConstraints ps) else do normed <- norm as return (normed, prog { prog_bindings = valBinds', prog_instances = instances' }) where ti classes instances binds = do -- insert the methods into the assumptions let methodsSigs = concatMap rwMethodSigs classes (names, schemes) = unzip methodsSigs as = buildAssumps names schemes `merge` initAs -- type the "regular" bindings (ps, as', binds') <- tiBindGroup TopLevel as binds let as'' = as' `merge` as -- check the types of the methods and resolve overloading instances' <- mapM (checkMethods as'') instances s <- gets ti_subst return (applySubst s ps, applySubst s as'', binds', instances') -- for a method declaration in class `D a1 .. aN', we must add the -- `D a1 .. aN' to the constraints and `a1 .. aN' to the quantified -- variables of its signature. rwMethodSigs :: ClassDec -> [VSig] rwMethodSigs cdec = let selfConstraint = CC $ ClassConstraint (class_name cdec) (map TyVar (class_params cdec)) rw (TypeScheme qs (QualifiedType cs t)) = TypeScheme (nub (class_params cdec ++ qs)) (QualifiedType (nub (selfConstraint : cs)) t) in map (\ (i,sc) -> (i, rw sc)) (class_vsigs cdec) checkMethods :: Assumps -> ClassInst -> TI ClassInst checkMethods as ci = do display ("checking methods of instance `" ++ showInstHead ci ++ "'") liftST $ addConcreteEqualities ci binds <- mapM (checkMethod as ci) (inst_valBinds ci) liftST $ deleteConcreteEqualities display ("finished checking methods of instance `" ++ showInstHead ci ++ "'") return (ci { inst_valBinds = binds }) checkMethod :: Assumps -> ClassInst -> ValBind -> TI ValBind checkMethod as ci bind@(ValBind i _ pats e _) = do let cid = inst_class ci -- we must construct the expected type of the implementation (_, TypeScheme qs (QualifiedType cs t)) <- liftST (findMethodSig cid i) cdec <- liftST $ findClass cid let cs' = inst_constraints ci ++ cs subst = substFromAssocs (zip (class_params cdec) (inst_types ci)) t' = applySubst subst t qs' = List.nub (qs ++ freeTypeVarsList (inst_types ci)) sc' = TypeScheme qs' (QualifiedType cs' t') debug ("checking definition of method " ++ showPpr' i ++ " in " ++ showInstHead ci ++ ". Expected type: " ++ showPpr' sc') (ps, (_, _, (pats', e'))) <- tiExpl as (i, sc', (pats, e)) let bind' = bind { vbind_pats = pats', vbind_exp = e' } if not (null ps) then panic ("Non-empty set of constraints after checking "++ "the type of a method: " ++ dumpAssumps as ++ "\n" ++ dumpConstraints ps) else do debug ("resolved overloading for method " ++ showPpr' i ++ ": " ++ showPpr' bind') return bind' norm :: Assumps -> ST Assumps norm as = do l <- mapM (\ (k, TypeScheme quants (QualifiedType ps t)) -> do t' <- runUF [] (normalise t) return (k, TypeScheme quants (QualifiedType ps t'))) (Map.assocs as) return $ Map.fromList l -- subsumes returns 2 substitution: -- -- The first is the substitution used for replacing the type variables in -- the user supplied type with fresh type constructors. -- -- The second is the substitution returned from the unification subsumes :: TypeScheme -> TypeScheme -> TI (Maybe (TypeSubst, TypeSubst)) subsumes sc1@(TypeScheme quants1 (QualifiedType pi1 tau1)) sc2@(TypeScheme quants2 qt2) = -- do not instantiate sc1, otherwise tiExpl will break! do debug $ "checking if " ++ showPpr' sc1 ++ " subsumes " ++ showPpr' sc2 kinds <- liftST $ mapM kindOf quants2 tycons <- liftST $ mapM freshTyConstruct kinds let subst = substFromAssocs (zip quants2 tycons) -- instantiate qt2 with the fresh type constructors QualifiedType pi2' tau2' = applySubst subst qt2 -- empty quantifier list is because quantified variables were -- replaced by fresh type constructors pi2Eqs = map (EqualityDefinition []) (eqConstraints pi2') ures <- liftST $ runUnify pi2Eqs [tau1 :=: tau2'] case ures of Left _ -> do debug "Subsumption check failed because unification failed" return Nothing Right (peqs, subst') -> do let pi1' = applySubst subst' pi1 xs <- liftST $ mapM (entail pi2') (pi1' ++ map EC peqs) if and xs then do debug "Subsumption succeeded" return (Just (subst, subst')) else do debug "Subsumption failed because entailment \ \failed" return Nothing {- if not (null peqs) then do debug "Subsumption failed because unification returned \ \non-empty pending equalities" return Nothing else do let pi1' = applySubst subst' pi1 xs <- liftST $ mapM (entail pi2') pi1' if and xs then do debug "Subsumption succeeded" return (Just (subst, subst')) else do debug "Subsumption failed because entailment \ \failed" return Nothing -} -- Overloading resolution is done during the generalization step. -- The list `recVars' contains the variables defined by the current binding -- group for which no context information is available during type inference. -- The list is empty for an explicitly type binding (because the type -- annotation has a context which is used during type inference). For an -- implicitly typed binding group, the list contains just the variables defined -- by the group. These variables will all have the context `ps' after -- generalization. generalize :: ValId -- variable whose signature is generalized -> [TypeVarId] -- type variables to generalize over -> [Constraint] -- context of the monotype -> Type -- the monotype -> TI TypeScheme generalize id gs ps t = do let sc = TypeScheme gs (QualifiedType ps t) checkForAmbiguity (id, sc) return sc tiResolveOverloading :: ValId -> [ValId] -- recursivly defined variables without context -- during type inference -> [ClassConstraint] -- class constraints of the binding -- and the recursivly defined -- variables -> Bind -- binding for which overloading resolution -- should take place -> TI Bind tiResolveOverloading id recVars cs bind = do let recMap = Map.fromList (zip recVars (repeat cs)) subst <- gets ti_subst debug ("resolving overloading for " ++ showPpr' id) bind' <- lift $ resolveOverloading subst recMap bind cs return bind' checkForAmbiguity :: (ValId, TypeScheme) -> TI () checkForAmbiguity (id, sc@(TypeScheme alphas rho)) = do let fv_rho = freeTypeVars rho fixv_rho = fixedTypeVars rho if not ((Set.fromList alphas `Set.intersection` fv_rho) `Set.isSubsetOf` fixv_rho) || -- because of the monomorphism restriction, signatures -- such as forall a . C b => a -> Int may arise so that -- we need an additional check (maybe this check is -- too restrictive, but this is ok for now) not (freeTypeVars (qtype_context rho) `Set.isSubsetOf` freeTypeVars (qtype_mono rho)) then phasefail ("ambiguous signature for " ++ showPpr' id ++ ": " ++ showPpr sc) else return () -- -- Helpers -- unzipConstraints :: [([ClassConstraint], [EqConstraint])] -> ([ClassConstraint], [EqConstraint]) unzipConstraints l = let (css, ess) = unzip l cs = concat css es = concat ess in (cs, es) freshInst :: TypeScheme -> TI ([Constraint], Type) freshInst sc = let quants = tyscheme_quants sc QualifiedType constrs ty = tyscheme_qtype sc in do ((constrs', ty'), _, _) <- liftST $ instantiate quants (constrs, ty) return (constrs', ty') toScheme :: Type -> TypeScheme toScheme t = TypeScheme [] (QualifiedType [] t) typeOfDataConstructor :: DataId -> ST TypeScheme typeOfDataConstructor di = do (tydef, dataCons) <- findDataConstructor di let quants = tydef_params tydef tc = TyConstruct (tydef_name tydef) resTy = foldl TyApp tc (map TyVar quants) t = tyFuns (dconstr_params dataCons) resTy return $ TypeScheme quants (QualifiedType [] t) funTypeId = builtinTypeId Builtins.funTypeConstructor intTypeId = builtinTypeId Builtins.intTypeConstructor boolTypeId = builtinTypeId Builtins.boolTypeConstructor charTypeId = builtinTypeId Builtins.charTypeConstructor intType = TyConstruct intTypeId boolType = TyConstruct boolTypeId tyFun :: Type -> Type -> Type tyFun t1 t2 = ((TyConstruct funTypeId) `TyApp` t1) `TyApp` t2 tyFuns :: [Type] -> Type -> Type tyFuns [] t = t tyFuns (t:ts) t2 = tyFun t (tyFuns ts t2) binIntTy = tyFuns [intType, intType] intType binCmpTy = tyFuns [intType, intType] boolType typeOfPrimOp :: Builtins.Op -> Type typeOfPrimOp Builtins.IntAddOp = binIntTy typeOfPrimOp Builtins.IntSubOp = binIntTy typeOfPrimOp Builtins.IntMulOp = binIntTy typeOfPrimOp Builtins.IntQuotOp = binIntTy typeOfPrimOp Builtins.IntRemOp = binIntTy typeOfPrimOp Builtins.IntNegOp = tyFun intType intType typeOfPrimOp Builtins.IntGtOp = binCmpTy typeOfPrimOp Builtins.IntGeOp = binCmpTy typeOfPrimOp Builtins.IntLtOp = binCmpTy typeOfPrimOp Builtins.IntLeOp = binCmpTy typeOfPrimOp Builtins.IntEqOp = binCmpTy typeOfPrimOp Builtins.IntNeOp = binCmpTy dumpTypeInference :: Assumps -> Program -> String dumpTypeInference as (Program _ classes _ binds) = let values = map dumpValue binds in concat (intersperse "\n" $ values) where dumpValue :: ValBind -> String dumpValue vb = dump (vbind_name vb) dump i = showTypeSig (i, (find i as)) showTypeSig (i, sc) = showPpr i ++ " :: " ++ showPpr sc showTypeSigs l = concat (intersperse "\n" $ map showTypeSig l)