[more work done on type inference (nearly complete, but nasty bug somewhere in unification) mail@stefanwehr.de**20050521115629] { hunk ./Builtins.hs 15 +-- +-- If you change something here, you also have to change TypeInference.hs +-- + hunk ./Builtins.hs 90 - -{- -typeOfPrimOp:: Op -> Type -typeOfPrimOp IntAddOp = binIntTy -typeOfPrimOp IntSubOp = binIntTy -typeOfPrimOp IntMulOp = binIntTy -typeOfPrimOp IntQuotOp = binIntTy -typeOfPrimOp IntRemOp = binIntTy -typeOfPrimOp IntNegOp = mkFunTy [intTyCon, intTyCon] -typeOfPrimOp IntGtOp = binCmpTy -typeOfPrimOp IntGeOp = binCmpTy -typeOfPrimOp IntLtOp = binCmpTy -typeOfPrimOp IntLeOp = binCmpTy -typeOfPrimOp IntEqOp = binCmpTy -typeOfPrimOp IntNeOp = binCmpTy - - --- --- builtin type constructors --- - -funTyCon = TyConstruct (mkIdFromString "->") -intTyCon = TyConstruct (mkIdFromString "Int") -boolTyCon = TyConstruct (mkIdFromString "Bool") -starTyCon = TyConstruct (mkIdFromString "(,)") -unitTyCon = TyConstruct (mkIdFromString "()") - -builtinTypeConstructors = - [funTyCon, intTyCon, boolTyCon, starTyCon, unitTyCon] - -binIntTy, binCmpTy :: Type -binIntTy = mkFunTy [intTyCon, intTyCon, intTyCon] -binCmpTy = mkFunTy [intTyCon, intTyCon, boolTyCon] - -mkFunTy :: [Type] -> Type -mkFunTy (t1:t2:[]) = TyApp (TyApp funTyCon t1) t2 -mkFunTy (t1:t2:ts) = TyApp (TyApp funTyCon t1) (mkFunTy (t2:ts)) -mkFunTy _ = panic "cannot make function type for less then 2 types" --} - hunk ./Entailment.hs 24 - catchST (runUnifyAssertEmpty eqEnv [t :=: t'] - >>= \s -> return (Just s)) - [UnificationFailed] (\_ -> return Nothing) + ures <- runUnifyAssertEmpty eqEnv [t :=: t'] + case ures of + Right s -> return $ Just s + Left err -> return Nothing hunk ./Entailment.hs 53 +-- entail uses the program's class and equality constraints implicitly hunk ./Entailment.hs 55 -entail ps (CC p) = +entail cs c = + do debug ("checking if " ++ dumpConstraints cs ++ " entails " ++ + showPpr' c) + answ <- entail' cs c + if answ + then debug (dumpConstraints cs ++ " entails " ++ showPpr' c) + else debug (dumpConstraints cs ++ " does not entail " ++ showPpr' c) + return answ + +entail' ps (CC p) = hunk ./Entailment.hs 73 -entail ps (EC (EqConstraint left right)) = +entail' ps (EC e@(EqConstraint left right)) = hunk ./Entailment.hs 78 - catchST (runUnifyAssertEmpty (eqEnv ++ ps') - [TyAssoc left :=: right] >> return True) - [UnificationFailed] (\_ -> return False) + ures <- runUnify (eqEnv ++ ps') [TyAssoc left :=: right] + case ures of + Right (peqs, _) -> return (null peqs) + Left _ -> return False hunk ./Error.hs 29 - debug_, enableDebug + debug_, enableDebug, + Location + hunk ./Error.hs 61 - show e = show progName ++ ": " ++ showPException e + show e = progName ++ ": " ++ showPException e hunk ./Error.hs 66 - show cause ++ "\n\t" ++ msg ++ "\n\n" + show cause ++ "\n\t" ++ msg hunk ./Error.hs 70 - = show cause ++ ":\n\t" ++ msg ++ "\n\n" + = show cause ++ ":\n\t" ++ msg hunk ./Error.hs 83 -catchFailure :: IO a -> [FailureCause] -> (FailureCause -> IO a) -> IO a +catchFailure :: IO a -> [FailureCause] -> (PException -> IO a) -> IO a hunk ./Error.hs 87 - if cause `elem` causes then handler cause + if cause `elem` causes then handler e hunk ./KindInference.hs 48 -kindApps' :: [Kind'] -> Kind' -> Kind' -kindApps' args result = +kindFun' :: [Kind'] -> Kind' -> Kind' +kindFun' args result = hunk ./KindInference.hs 282 -kindInference :: Program -> ST Program +kindInference :: Program -> ST () hunk ./KindInference.hs 298 --- we have to rewrite the program by replacing the dummy kinds of the --- type variables with the correct ones. -correctKinds :: Program -> KI Program + +correctKinds :: Program -> KI () hunk ./KindInference.hs 301 - Gen.everywhereM (Gen.mkM correct) p + do Gen.everywhereM (Gen.mkM correct) p + return () hunk ./KindInference.hs 341 - let typeDefKind = kindApps' argKinds Star + let typeDefKind = kindFun' argKinds Star hunk ./KindInference.hs 370 - let assocTypeKind = kindApps' (indexKind:restKinds) resultKind + let assocTypeKind = kindFun' (indexKind:restKinds) resultKind hunk ./KindInference.hs 409 - unify atKind (kindApps' (indexKind:paramKinds) resKind) + unify atKind (kindFun' (indexKind:paramKinds) resKind) hunk ./KindInference.hs 444 - unify k (kindApps' paramKinds resultKind) + unify k (kindFun' paramKinds resultKind) hunk ./Kinds.hs 27 - return $ kindApps paramKinds KindStar + return $ kindFun paramKinds KindStar hunk ./Kinds.hs 32 - return $ kindApps paramKinds KindStar + return $ kindFun paramKinds KindStar hunk ./Main.hs 38 +import TypeInference hunk ./Main.hs 66 - ast' <- kindInference ast - WFP.checkAfterKindInference ast' + kindInference ast + WFP.checkAfterKindInference ast hunk ./Main.hs 69 - do liftIO $ dump (ppr ast') - kiDump <- dumpKindInference ast' + do liftIO $ dump (ppr ast) + kiDump <- dumpKindInference ast hunk ./Main.hs 72 + tiMain ast hunk ./Main.hs 92 + hPutStrLn stderr "" hunk ./Main.hs 96 + hPutStrLn stderr "" hunk ./ParseSyntax.hs 134 -splitConstraitns (x:xs) = +splitConstraints (x:xs) = hunk ./ParseSyntax.hs 152 + +dumpClassConstraints :: [ClassConstraint] -> String +dumpClassConstraints cs = + "{ClassConstraints: " ++ + showCommaListed (map ppr cs) + ++ "}" + +dumpEqConstraints :: [EqConstraint] -> String +dumpEqConstraints es = + "{EqConstraints: " ++ + showCommaListed (map ppr es) + ++ "}" + +dumpConstraints :: [Constraint] -> String +dumpConstraints cs = + "{Constraints: " ++ + showCommaListed (map ppr cs) + ++ "}" + hunk ./ParseSyntax.hs 189 -kindApps :: [Kind] -> Kind -> Kind -kindApps args result = +kindFun :: [Kind] -> Kind -> Kind +kindFun args result = hunk ./ParseSyntax.hs 200 -tyApps :: [Type] -> Type -> Type -tyApps args result = - foldr TyApp result args - hunk ./ParseSyntax.hs 210 +splitQType :: QualifiedType -> ([Constraint], Type) +splitQType (ConstrainedType cs t) = (cs, t) +splitQType (UnconstrainedType t) = ([], t) + hunk ./ParseSyntax.hs 421 + +instance Pretty EqScheme where + pprPrec prec (EqScheme vars ec) = + if null vars + then pprPrec prec ec + else pprInfixOp prec eqConstraintSpec + (text "forall" <+> ppr vars) + (space <> char '.' <> space) + ec hunk ./Pretty.hs 23 - printDoc, showPpr, showList, showCommaListed, + printDoc, showPpr, showPpr', showList, showCommaListed, hunk ./Pretty.hs 59 + hunk ./Pretty.hs 61 - pprPrec prec s = hcat $ map (pprPrec prec) s + pprPrec prec s = + parens `usedWhen` (prec > minPrec) $ hsep (map (pprPrec maxPrec) s) + hunk ./Pretty.hs 69 +showPpr' :: Pretty p => p -> String +showPpr' p = show $ text "`" <> ppr p <> text "'" + hunk ./Pretty.hs 78 - show $ pprList ", " l + show $ text "{" <> pprList ", " l <> text "}" hunk ./Substitution.hs 44 - "[" ++ + "{" ++ hunk ./Substitution.hs 47 - ++ "]" + ++ "}" hunk ./Symtab.hs 15 - instantiate, freshTypeVar + instantiate, freshTypeVar, freshTyConstruct hunk ./Symtab.hs 35 - typeVarVersion :: UniqIdents.Version, -- next free type var version + version :: UniqIdents.Version, -- next free version hunk ./Symtab.hs 43 - typeVarVersion = UniqIdents.initialVersion - 1, + version = UniqIdents.initialVersion - 1, hunk ./Symtab.hs 53 -catchST :: ST a -> [FailureCause] -> (FailureCause -> ST a) -> ST a +catchST :: ST a -> [FailureCause] -> (PException -> ST a) -> ST a hunk ./Symtab.hs 130 - do cur <- gets typeVarVersion - modify (\s -> s { typeVarVersion = cur - 1 }) + do cur <- gets version + modify (\s -> s { version = cur - 1 }) hunk ./Symtab.hs 140 + +freshTyConstruct :: Kind -> ST Type +freshTyConstruct kind = + do cur <- gets version + modify (\s -> s { version = cur - 1 }) + let id = UniqIdents.mkTypeId "C" cur + args <- freshArgs kind + let tydef = TypeDef id args [] + insertTypeDef tydef + return (TyConstruct id) + where freshArgs KindStar = return [] + freshArgs (KindFun k1 k2) = + do v <- freshTypeVar' k1 + restArgs <- freshArgs k2 + return (v:restArgs) hunk ./SyntaxTransformation.hs 53 - do --addBuiltIns - -- add forward declarations (but only those which are really needed) + do -- add forward declarations (but only those which are really needed) addfile ./TypeInference.hs hunk ./TypeInference.hs 1 +module TypeInference where + +import Control.Monad.State +import Control.Monad.Error +import qualified Map +import qualified Data.Set as Set +import qualified Builtins +import UniqIdents ( builtinTypeId ) +import Builtins +import AbstractSyntax +import Substitution +import Error +import Pretty +import Symtab +import Unification hiding (unify) +import Entailment ( entail, split, reduce ) +import Kinds + +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") + +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 + eqEnv <- liftST getEqEnv + let eq = (applySubst s t1) :=: (applySubst s t2) + eqs = map toTypeEq (applySubst s eqc) + ures <- liftST $ runUnify eqEnv (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 (([ClassConstraint], [EqConstraint]), t) + +tiExpr :: Infer Exp Type +tiExpr as (Var i) = + do let sc = find i as + (ps, t) <- freshInst sc + return (splitConstraints ps, t) + +tiExpr as (Num _) = return $ (([], []), TyConstruct intTypeId) + +tiExpr as (Prim op es) = + do l <- mapM (tiExpr as) es + alpha <- liftST $ freshTypeVar KindStar + let (constrs, operandTypes) = unzip l + opTy = typeOfPrimOp op + resTy = tyFuns operandTypes alpha + unify [] opTy resTy + return (unzipConstraints constrs, alpha) + +tiExpr as (App e1 e2) = + do ((theta1, u1), tau1) <- tiExpr as e1 + ((theta2, u2), tau2) <- tiExpr as e2 + alpha <- liftST $ freshTypeVar KindStar + u <- unify (u1 ++ u2) tau1 (tau2 `tyFun` alpha) + return ((theta1 ++ theta2, u), alpha) + +-- \x1 .. xN -> e is rewritten as \x1 -> .. \xN -> e +tiExpr as (Lam [] e) = tiExpr as e +tiExpr as (Lam (x:xs) e) = + do alpha <- liftST $ freshTypeVar KindStar + (ps, tau) <- tiExpr (add x (toScheme alpha) as) (Lam xs e) + return (ps, alpha `tyFun` tau) + +tiExpr as (Letrec binds e) = + do ((ps, psEq), as') <- tiBindGroup as binds + ((qs, qsEq), t) <- tiExpr (as' `merge` as) e + return ((ps ++ qs, psEq ++ qsEq), t) + +-- the Bind type here corresponds to the Alt type in THIH +type Bind = ([ValId] {- arguments -} , Exp) + +tiBind :: Infer Bind Type +tiBind as (is, e) = + do alphas <- mapM (\_ -> liftST $ freshTypeVar KindStar) is + let ts = map toScheme alphas + as' = buildAssumps is ts + (qs, t) <- tiExpr (as' `merge` as) e + let resTy = tyFuns alphas t + return (qs, resTy) + + +subsumes :: TypeScheme -> TypeScheme -> TI Bool +subsumes sc1@(TypeScheme quants1 qt1) sc2@(TypeScheme quants2 qt2) = + 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 + qt2' = applySubst subst qt2 + (pi2', tau2') = splitQType qt2' + -- empty EqScheme is because quantified variables were replaced + -- by fresh type constructors + pi2Eqs = map (EqScheme []) (eqConstraints pi2') + (pi1, tau1) = splitQType qt1 + eqEnv <- liftST getEqEnv + ures <- liftST $ runUnify (eqEnv ++ pi2Eqs) [tau1 :=: tau2'] + case ures of + Left _ -> + do debug "Subsumption check failed because unification failed" + return False + Right (peqs, subst) -> + if not (null peqs) + then do debug "Subsumption failed because unification returned \ + \non-empty pending equalities" + return False + else do let pi1' = applySubst subst pi1 + xs <- liftST $ mapM (entail pi2') pi1' + if and xs + then do debug "Subsumption succeeded" + return True + else do debug "Subsumption failed because entailment \ + \failed" + return False + + +type Expl = (ValId, TypeScheme, Bind) + +-- returns the deferred constraints +tiExpl :: Assumps -> Expl -> TI ([ClassConstraint], [EqConstraint]) +tiExpl as (i, sc, bind) = + do (ps, t) <- tiBind as bind -- infered type + (qs, x) <- freshInst sc -- user supplied type + unify [] t x -- important + s <- gets ti_subst + let t' = applySubst s t + ps' = mergeConstraints $ applySubst s ps + fs = freeTypeVars (applySubst s as) + gs = (freeTypeVars ps' `Set.union` freeTypeVars t') + `Set.difference` fs + sc' = TypeScheme (Set.toList gs) + (if null ps' then UnconstrainedType t' + else ConstrainedType ps' t') + b <- subsumes sc' sc + if not b + then phasefail ("type error while checking explicitly typed binding `" + ++ showPpr i ++ "': user-supplied signature too " ++ + "general\n infered signature: " + ++ showPpr sc' ++ "\n user-supplied signature: " + ++ showPpr sc) + else return () + -- simplification + let qs' = applySubst s qs + ps'' <- liftST $ filterM ((liftM not) . entail qs') ps' + (ds, rs) <- liftST $ split (Set.toList fs) (Set.toList gs) ps'' + if not (null rs) + then panic ("While typing explicitly typed binding: " ++ + "list of retained constraints is not empty, " ++ + "although subsumption check was successful\n" ++ + " infered type: " ++ showPpr sc' ++ + "\n user-supplied type: " ++ showPpr sc ++ + "\n defered constraints: " ++ showPpr ds ++ + "\n retained constraints: " ++ showPpr rs) + else do debug (showPpr i ++ " :: " ++ showPpr sc) + return $ splitConstraints ds + + +type Impl = (ValId, Bind) + +-- returns the deferred constraints and the types for the bindings +tiImpls :: Infer [Impl] Assumps +tiImpls as bs = + do -- type for every bindind + ts <- liftST $ mapM (\_ -> freshTypeVar KindStar) bs + let is = map fst bs + scs = map toScheme ts + as' = as `merge` buildAssumps is scs + l <- mapM (tiBind as') (map snd bs) + let (constrs, types) = unzip l + ps = mergeConstraints (unzipConstraints constrs) + mapM (uncurry $ unify []) (zip ts types) + s <- gets ti_subst + let ps' = applySubst s ps + ts' = applySubst s ts + fs = freeTypeVars (applySubst s as) + vss = map freeTypeVars ts' + gs = Set.unions vss `Set.difference` fs + (ds, rs) <- liftST $ split (Set.toList fs) + (Set.toList $ foldr1 Set.intersection vss) + ps' + if restricted bs + then + let gs' = gs `Set.difference` (freeTypeVars rs) + scs' = map (\t -> TypeScheme (Set.toList gs') + (UnconstrainedType t)) ts' + in return (splitConstraints (ds ++ rs), buildAssumps is scs') + else + let scs' = map (\t -> TypeScheme (Set.toList gs) + (ConstrainedType rs t)) ts' + in return (splitConstraints ds, buildAssumps is scs') + where + restricted :: [Impl] -> Bool + restricted bs = + let simple (i, b) = null (fst b) + in any simple bs + + + +-- FIXME: need depend analysis +tiBindGroup :: Infer [ValBind] Assumps +tiBindGroup as binds = + do let (as', expls, impls) = collect emptyAssumps binds + (ps, as'') <- tiImpls (as' `merge` as) impls + qss <- mapM (tiExpl (as'' `merge` as' `merge` as)) expls + let resConstrs = unzipConstraints qss + resAssumps = as'' `merge` as' + mapM checkForAmbiguity (Map.assocs resAssumps) + return (resConstrs, resAssumps) + where + collect as [] = (as, [], []) + collect _ (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) + checkForAmbiguity :: (ValId, TypeScheme) -> TI () + checkForAmbiguity (id, sc@(TypeScheme alphas rho)) = + let fv_rho = freeTypeVars rho + fixv_rho = fixedTypeVars rho + in if not ((Set.fromList alphas `Set.intersection` fv_rho) + `Set.isSubsetOf` fixv_rho) + then phasefail ("ambiguous signature for " ++ showPpr' id + ++ ": " ++ showPpr sc) + else return () + + +tiMain :: Program -> ST () +tiMain (Program _ _ _ valBinds) = + do ((cs,es), as) <- runTI $ ti emptyAssumps valBinds + liftIO $ putStrLn (dumpAssumps as) + liftIO $ putStrLn (dumpClassConstraints cs) + liftIO $ putStrLn (dumpEqConstraints es) + return () + where ti as binds = + do (ctx, as') <- tiBindGroup as binds + s <- gets ti_subst + return (applySubst s ctx, applySubst s as') + +-- +-- 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 + (constrs, ty) = case tyscheme_qtype sc of + UnconstrainedType t -> ([], t) + ConstrainedType cs t -> (cs, t) + in do ((constrs', ty'), _) <- liftST $ instantiate quants (constrs, ty) + return (constrs', ty') + +toScheme :: Type -> TypeScheme +toScheme t = TypeScheme [] (UnconstrainedType t) + +funTypeId = builtinTypeId Builtins.funTypeConstructor +intTypeId = builtinTypeId Builtins.intTypeConstructor +boolTypeId = builtinTypeId Builtins.boolTypeConstructor + +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 hunk ./Unification.hs 11 +import Control.Monad.Error hunk ./Unification.hs 14 -import List (intersperse) +import List (intersperse, nub) hunk ./Unification.hs 59 + Just s -> return s hunk ./Unification.hs 61 - hunk ./Unification.hs 67 - deriving (Show) + deriving (Show,Eq) hunk ./Unification.hs 76 - "[" ++ + "{" ++ hunk ./Unification.hs 79 - ++ "]" + ++ "}" hunk ./Unification.hs 86 -type UFResult = ([TypeEq], TypeSubst) +type UFResult' = ([TypeEq], TypeSubst) hunk ./Unification.hs 96 -catchUF :: UF a -> [FailureCause] -> (FailureCause -> UF a) -> UF a +catchUF :: UF a -> [FailureCause] -> (PException -> UF a) -> UF a hunk ./Unification.hs 106 -reduceOneStep :: Type -> UF Type +reduceOneStep t = + do debug ("reduceOneStep: " ++ showPpr t) + res <- reduceOneStep' t + debug "reduceOneStep DONE" + return res + +reduceOneStep' :: Type -> UF Type hunk ./Unification.hs 114 -reduceOneStep (TyApp t1 t2) = +reduceOneStep' (TyApp t1 t2) = hunk ./Unification.hs 121 -reduceOneStep (TyAssoc (AssocType id params)) = +reduceOneStep' (TyAssoc at@(AssocType id params)) = hunk ./Unification.hs 126 - liftST $ reduceAT id params constrs + debug "calling reduceAT" + res <- liftST $ reduceAT at constrs + debug "after reduceAT" + return res hunk ./Unification.hs 142 - reduceAT :: AssocTypeId -> [Type] -> EqEnv -> ST Type - reduceAT id params [] = - failwith ReductionFailed ("cannot reduce type synonym " ++ showPpr id) - reduceAT id params (EqScheme quants eq : rest) = + reduceAT :: AssocType -> EqEnv -> ST Type + reduceAT at [] = + failwith ReductionFailed ("cannot reduce type synonym " ++ showPpr' at) + reduceAT at@(AssocType id params) (sc@(EqScheme quants eq) : rest) = hunk ./Unification.hs 147 - then reduceAT id params rest - else do -- instantiate the scheme + then reduceAT at rest + else do debug ("Trying to use equality scheme " ++ showPpr' sc ++ + " for reducing " ++ showPpr' at) + -- instantiate the scheme hunk ./Unification.hs 160 + let res = applySubst subst (eqc_right eq') + debug ("reduction successful, result: " ++ showPpr' res) hunk ./Unification.hs 165 - (return $ applySubst subst (eqc_right eq')) + (return res) hunk ./Unification.hs 167 -reduceOneStep t = failwith ReductionFailed ("cannot reduce " ++ showPpr t) +reduceOneStep' t = + do debug ("cannot reduce " ++ showPpr t) + failwith ReductionFailed ("cannot reduce " ++ showPpr t) hunk ./Unification.hs 177 -unifyOneStep :: TypeEq -> UF UFResult +unifyOneStep eq = + do debug "unifyOneStep" + res <- unifyOneStep' eq + debug "unifyOneStep DONE" + return res + +unifyOneStep' :: TypeEq -> UF UFResult' hunk ./Unification.hs 185 -unifyOneStep (t1 :=: t2) | t1 == t2 = return (emptyEqs, nullSubst) +unifyOneStep' (t1 :=: t2) | t1 == t2 = return (emptyEqs, nullSubst) hunk ./Unification.hs 187 -unifyOneStep (TyVar u :=: t) = oneStepVar u t -unifyOneStep (t :=: TyVar u) = oneStepVar u t +unifyOneStep' (TyVar u :=: t) = oneStepVar u t +unifyOneStep' (t :=: TyVar u) = oneStepVar u t hunk ./Unification.hs 190 -unifyOneStep (TyApp l r :=: TyApp l' r') = +unifyOneStep' (TyApp l r :=: TyApp l' r') = hunk ./Unification.hs 193 -unifyOneStep (t1@(TyAssoc _) :=: t2) = oneStepAssoc t1 t2 -unifyOneStep (t1 :=: t2@(TyAssoc _)) = oneStepAssoc t1 t2 +unifyOneStep' (t1@(TyAssoc _) :=: t2) = oneStepAssoc t1 t2 +unifyOneStep' (t2 :=: t1@(TyAssoc _)) = oneStepAssoc t1 t2 +-- default +unifyOneStep' (t1 :=: t2) = + failwith UnificationFailed ("cannot unify `" ++ showPpr t1 ++ "' with `" ++ + showPpr t2 ++ "'") hunk ./Unification.hs 200 -oneStepVar :: TypeVarId -> Type -> UF UFResult +oneStepVar :: TypeVarId -> Type -> UF UFResult' hunk ./Unification.hs 214 -oneStepAssoc :: Type -> Type -> UF UFResult +oneStepAssoc :: Type -> Type -> UF UFResult' hunk ./Unification.hs 225 -runUnifyAssertEmpty :: EqEnv -> [TypeEq] -> ST TypeSubst +-- Unification does not use the program's equality constraints automatically. +-- All assumptions must be supplied explicitly in the first parameter +-- of type EqEnv (functions runUnifyAssertEmpty, runUnify, runUF). + +type UFResult = Either String ([EqConstraint], TypeSubst) + +runUnifyAssertEmpty :: EqEnv -> [TypeEq] -> ST (Either String TypeSubst) hunk ./Unification.hs 233 - do (peqs, subst) <- runUnify env eqs - if null peqs - then return subst - else panic - ("Unification should finished without pending equalities, " ++ - "but some equalities are left: " ++ showCommaListed peqs) + do res <- runUnify env eqs + case res of + Left err -> return $ Left err + Right (peqs, subst) -> + if null peqs + then return $ Right subst + else panic + ("Unification should finished without pending " ++ + "equalities, but some equalities are left: " + ++ showCommaListed peqs) hunk ./Unification.hs 244 -runUnify :: EqEnv -> [TypeEq] -> ST ([EqConstraint], TypeSubst) +runUnify :: EqEnv -> [TypeEq] -> ST UFResult hunk ./Unification.hs 247 -unify :: [TypeEq] -> UF ([EqConstraint], TypeSubst) +unify :: [TypeEq] -> UF UFResult hunk ./Unification.hs 249 - do debug ("running unification on " ++ showEqs eqs) + do theta <- gets uf_theta + debug ("running unification on " ++ showEqs eqs ++ + " under the assumptions " ++ showCommaListed theta) hunk ./Unification.hs 257 - let u' = map adjustConstraint u - debug ("unification finished, substitution: " ++ showSubst r ++ - "\n pending equality constraints: " ++ showCommaListed u') - return (u', r) + case mapM adjustConstraint u of + Right u' -> + do debug ("unification finished, substitution: " ++ showSubst r ++ + ", pending equality constraints: " ++ showCommaListed u') + return $ Right (u', r) + Left err -> + do debug ("Unification failed: " ++ err) + return $ Left err hunk ./Unification.hs 272 - _ -> EqConstraint at t + _ -> Right $ EqConstraint at t hunk ./Unification.hs 274 - failwith UnificationFailed - ("Cannot unify " ++ showEqs eqs ++ - ". Unsatisfiable equality constraint: " ++ showPpr c) + Left ("Cannot unify " ++ showEqs eqs ++ + ". Unsatisfiable equality constraint: " ++ showPpr c) hunk ./Unification.hs 277 -unify' :: [TypeEq] -> UF UFResult +unify' :: [TypeEq] -> UF UFResult' hunk ./Unification.hs 279 - do x <- tryOneStep eqs + do debug ("unify' " ++ showEqs eqs) + x <- tryOneStep eqs hunk ./Unification.hs 289 - (\_ -> err) + (\e -> do debug (show e) + err) hunk ./Unification.hs 295 - do (u',r') <- unifyOneStep eq + do debug "tryOneStep" + (u',r') <- unifyOneStep eq hunk ./UniqIdents.hs 28 - mkTypeVar + mkTypeVar, mkTypeId hunk ./UniqIdents.hs 315 + +mkTypeId :: String -> Version -> TypeId +mkTypeId s v = + if v >= initialVersion + then panic ("mkTypeId called with illegal version number: " ++ + show v) + else (TypeId (Id v s)) + hunk ./WellFormedProgram.hs 58 - in catchST (tryUnify t1 t2) - [UnificationFailed] (\_ -> return False) - tryUnify t1 t2 = - do (eqc, _) <- runUF [] (unify [t1 :=: t2]) - if null eqc then return True - else panic - ("Unification succeeded with the following equality " - ++ "constraints when checking for overlapping " - ++ "instances: " ++ showCommaListed eqc) -{- - do catchST (unifyTypes (inst_type i1) (inst_type i2) - >> return True) - [UnificationFailed] (\_ -> return False) --} + in do eqEnv <- getEqEnv + ures <- runUnify eqEnv [t1 :=: t2] + case ures of + Left err -> return False + Right (eqc, _) -> + if null eqc + then return True + else panic ("Unification succeeded with the " ++ + "following equality " + ++ "constraints when checking for " ++ + "overlapping instances: " ++ + showCommaListed eqc) hunk ./pp/macros.m4 8 +define(__loc__, (`SRC_LOC_'))dnl addfile ./tests/well-formed/should_fail/overlapping2.mhs hunk ./tests/well-formed/should_fail/overlapping2.mhs 1 +class C1 a where { + type T1 a; +} + +class C2 a where { + type T2 a; +} + +instance C1 Int where { + type T1 Int = Bool; +} + +instance C2 Bool where { + type T2 Bool = Unit; +} + +instance C2 (T1 Int) where { + type T2 (T1 Int) = Int; +} + }