[added overloading resolution mail@stefanwehr.de**20050530224659] { adddir ./tests/overloading-resolution adddir ./tests/overloading-resolution/should_pass hunk ./Entailment.hs 32 --- --- standard Haskell typeclass entailment --- - --- `matchConstraint (A, ts) c' checks if the constraint c is fulfilled --- by the instance declaration A ts. -matchConstraint :: (ClassId, [Type]) -> ClassConstraint -> ST (Maybe TypeSubst) -matchConstraint (id, ts) (ClassConstraint id' ts') - | id /= id' - = return Nothing - | otherwise - = do -- first normalize the type - tns <- runUF [] (mapM normalise ts) - tns' <- runUF [] (mapM normalise ts') - -- then use match to see if there is a substitution s such that - -- applySubst s t = t' - matchTypes tns tns' - hunk ./Entailment.hs 60 - where tryInst ci = + where tryInst ci = hunk ./IdMap.hs 75 -dumpMap :: (Pretty k, Pretty a) => Map.Map k a -> Doc -dumpMap m = hcat $ - punctuate (text ", ") - (map (\ (k,v) -> ppr k <+> text "-->" <+> ppr v) - (Map.assocs m)) - hunk ./Main.hs 41 +import Overloading hunk ./Main.hs 52 -import List (find) +import List ( find ) +import Maybe ( isJust ) hunk ./Main.hs 91 - as <- tiMain emptyAssumps bast + (as, bast') <- tiMain emptyAssumps bast hunk ./Main.hs 95 - setFreshVarsPrefix "v" "C" - as' <- tiMain as ast + setFreshVarsPrefix "v" "C" "d" + (as', ast') <- tiMain as ast hunk ./Main.hs 99 + + installInstanceDictionaries (AS.prog_instances bast' ++ + AS.prog_instances ast') hunk ./Main.hs 103 + when (on $ Dump OverReso) $ + do let isBuiltin ((cid, ts), _) = + isJust (find (\ci -> AS.inst_class ci == cid && + AS.inst_types ci == ts) + (AS.prog_instances bast')) + dictExprs <- getDictionaryExpressions + liftIO $ dump (dumpDictExprs (filter (not . isBuiltin) + dictExprs)) + liftIO $ dump (AS.prog_bindings ast') hunk ./Main.hs 234 + | OverReso hunk ./Main.hs 250 - "be verbose (but not as much as with `--debug'" + "be verbose (but not as much as with `--debug')" hunk ./Main.hs 264 - "print syntax after type inference" + "print kinds after kind inference" hunk ./Main.hs 267 + , Option [] ["dump-over"] (NoArg (Dump OverReso)) + "print syntax after overloading resolution" addfile ./Overloading.hs hunk ./Overloading.hs 1 +{-# OPTIONS_GHC -fglasgow-exts #-} + +-- +-- 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 Overloading ( + + resolveOverloading, Bind, installInstanceDictionaries, + dumpDictExprs +) where + +import qualified Data.Map as Map +import Control.Monad.State + +import Symtab +import AbstractSyntax +import Error +import Unification ( matchConstraint ) +import Pretty +import Substitution +import Pretty + +{- + +The dictionary resolution algorithm is based on "John Peterson and +Mark Jones. Implementing Type Classes. PLDI '93". + +-} + + + +data OVState = OVState { -- the current substitution + ov_subst :: TypeSubst, + -- context information for recursivly defined variables + ov_recMap :: RecMap, + -- mapping from class constraints to dictionary + -- variables providing evidence for the constraint + ov_dictEnv :: DictEnv + } + +type OV = StateT OVState ST + +runOV :: TypeSubst -- current substitution + -> RecMap -- context for recursivly defined variables + -> [(ClassConstraint, ValId)] -- mapping from class constraints to + -- dictionary variables for the binding + -- being translated + -> OV a -- OV computation to run + -> ST a +runOV subst map pairs ov = + do env <- buildDictEnv pairs + evalStateT ov (OVState subst map env) + + +type RecMap = Map.Map ValId [ClassConstraint] +emptyRecMap = Map.empty + + +-- The dictionary environment. +-- +-- Maps class constraints to variable names holding the dictionaries +-- for the constraints. If there is a mapping from `C a1 .. aN' to +-- some variable, there must be mappings for all super classes of `C' +-- to the same variable. Use the `buildDictEnv' function to maintain this +-- invariant. +type DictEnv = Map.Map ClassConstraint ValId +emptyDictEnv = Map.empty + +buildDictEnv :: [(ClassConstraint, ValId)] -> ST DictEnv +buildDictEnv pairs = foldM ins emptyDictEnv pairs + where ins env (cc@(ClassConstraint c t), id) = + do supers <- findAllSuperClasses c + let constrs = cc : map (\c -> ClassConstraint c t) supers + return (foldl (\m k -> Map.insert k id m) env constrs) + +installInstanceDictionaries :: [ClassInst] -> ST () +installInstanceDictionaries insts = + do replaceInstances insts -- replace the instances in the symtab + let keys = map (\ci -> (inst_class ci, inst_types ci)) insts + dictExps <- mapM buildInstanceDictionary insts + mapM (uncurry enterDictionaryExpression) (zip keys dictExps) + return () + +{- + Returns an expression which yields a dictionary for the given instance + when applied to the appropriate arguments. The arguments correspond + to the constraints in the instance context. + + A dictionary is just a list containing the code of all methods of the + instance (this includes the methods of all superclasses). + + See {tests/overloading-resolution/should_pass/004.phc, + tests/overloading-resolution/should_pass/005.phc} + for how dictionaries look like. +-} +buildInstanceDictionary :: ClassInst -> ST Exp +buildInstanceDictionary ci = + do let (cs,_) = splitConstraints (inst_constraints ci) + ds <- mapM (\_ -> freshValVar) cs + let instanceMapping = map (methodEntry ds) (inst_valBinds ci) + -- construct dictionaries for super classes + supers <- findAllSuperClasses (inst_class ci) + let superConstrs = map (\c -> ClassConstraint c (inst_types ci)) supers + superExps <- runOV nullSubst emptyRecMap (zip cs ds) $ + mapM getDictionaryExp superConstrs + superMapping <- mapM superEntries (zip supers superExps) + return (Lam ds (Overloading $ + Dictionary (instanceMapping ++ concat superMapping))) + where + methodEntry :: [ValId] -> ValBind -> (ValId, Exp) + methodEntry ctxParams bind = + let {- selfFun = Overloading $ + DictionaryReference (inst_class ci) (inst_types ci) + self = foldl App selfFun (map Var ctxParams) -} + e = foldl App (Lam (vbind_params bind) (vbind_exp bind)) + (map Var ctxParams) + in (vbind_name bind, e) + superEntries :: (ClassId, Exp) -> ST [(ValId, Exp)] + superEntries (cid, e) = + do mids <- getMethods cid + return (map (\i -> (i, Overloading $ DictionaryLookup i e)) mids) + + +-- Returns the instance declaration which fulfills the given constraint. +-- Additionally, the class constraints in the instance context are returned, +-- after applying the appropriate substitution. +-- If there is no instance declaration fulfilling the constraint, +-- `Nothing' is returned. This can happen with deferred constraints. +getInstance :: ClassConstraint -> ST (Maybe (ClassInst, [ClassConstraint])) +getInstance c@(ClassConstraint i _) = + do insts <- findInstances i + candidates <- sequence [tryInst it | it <- insts] + case msum candidates of + Nothing -> + return Nothing + Just (ci, goals) -> + let (cs, _) = splitConstraints goals + in return $ Just (ci, cs) + where tryInst ci = + do u <- matchConstraint (inst_class ci, inst_types ci) c + case u of + Nothing -> return Nothing + Just u' -> + return $ Just (ci, map (applySubst u') + (inst_constraints ci)) + +{- + Returns a expression evaluating to a dictionary which provides evidence + for the given constraint. +-} +getDictionaryExp :: ClassConstraint -> OV Exp +getDictionaryExp c = + do env <- gets ov_dictEnv + case Map.lookup c env of + Just id -> return $ Var id + Nothing -> + do inst <- lift $ getInstance c + case inst of + Nothing -> + return $ Overloading (Placeholder c) -- deferred constraint + Just (ci, cs) -> + do dicts <- mapM getDictionaryExp cs + let instDict = DictionaryReference (inst_class ci) + (inst_types ci) + return $ foldl App (Overloading instDict) dicts + + +resolveExp :: Exp -> OV Exp + +resolveExp (Overloading (Placeholder c)) = + do s <- gets ov_subst + getDictionaryExp (applySubst s c) + +resolveExp (Overloading (MethodPlaceholder cid mid ts)) = + do s <- gets ov_subst + let ts' = applySubst s ts + dexp <- getDictionaryExp (ClassConstraint cid ts') + return $ Overloading (DictionaryLookup mid dexp) + +resolveExp (Overloading o) = + panic ("unexpected Overloading value during overloading resolution: " ++ + show o) + +resolveExp (Var id) = + do recMap <- gets ov_recMap + case Map.lookup id recMap of + Nothing -> + return (Var id) + Just [] -> + do debug ("no overloading resolution necessary for recursivly " ++ + "defined variable " ++ showPpr' id) + return (Var id) + Just cs -> + do ds <- mapM getDictionaryExp cs + let e = foldl App (Var id) ds + debug ("resolving overloading for recursivly defined " ++ + "variable " ++ showPpr' id ++ " by replacing it with " + ++ showPpr' e) + return e + +resolveExp e@(Const _) = return e +resolveExp (Prim op es) = + do es' <- mapM resolveExp es + return $ Prim op es' +resolveExp (Con id es) = + do es' <- mapM resolveExp es + return $ Con id es' +resolveExp (App e1 e2) = + do e1' <- resolveExp e1 + e2' <- resolveExp e2 + return $ App e1' e2' +resolveExp (Lam vs e) = + do e' <- resolveExp e + return $ Lam vs e' +resolveExp (If e1 e2 e3) = + do e1' <- resolveExp e1 + e2' <- resolveExp e2 + e3' <- resolveExp e3 + return $ If e1' e2' e3' +resolveExp (Letrec vs e) = + do e' <- resolveExp e + return $ Letrec vs e' +resolveExp (Case e alts) = + do e' <- resolveExp e + alts' <- mapM resolveAlt alts + return $ Case e' alts' + where resolveAlt a = + do e' <- resolveExp (alt_exp a) + return $ a { alt_exp = e' } +resolveExp (Error s) = return (Error s) + + +type Bind = ([ValId] {- arguments -} , Exp) + +resolveOverloading :: TypeSubst -- the current substitution + -> RecMap -- constraints for recursivly defined vars + -> Bind -- the binding to transform + -> [ClassConstraint] -- class context of the binding + -> ST Bind -- the transformed binding +resolveOverloading subst recMap (params, e) cs = + do debug ("resolveOverloading called with recMap=" ++ show (dumpMap recMap) + ++ ", cs=" ++ showCommaListed cs) + ds <- mapM (\_ -> freshValVar) cs + e' <- runOV subst recMap (zip cs ds) (resolveExp e) + return (ds ++ params, e') + + +dumpDictExprs :: [((ClassId, [Type]), Exp)] -> Doc +dumpDictExprs [] = empty +dumpDictExprs (((cid, ts), e) : rest) = + let restDoc = dumpDictExprs rest + doc = text "dict-" <> ppr cid <> text "<" <> pprList ", " ts + <> text ">:" $$ ppr e + in doc $$ restDoc hunk ./ParseSyntax.hs 78 -data Program = Program [TypeDef] [ClassDec] [ClassInst] [ValBind] +data Program = Program { prog_typeDefs :: [TypeDef], + prog_classes :: [ClassDec], + prog_instances :: [ClassInst], + prog_bindings :: [ValBind] + } hunk ./ParseSyntax.hs 136 - deriving (Read, Show, Eq, Gen.Data, Gen.Typeable) + deriving (Read, Show, Eq, Ord, Gen.Data, Gen.Typeable) hunk ./ParseSyntax.hs 229 - deriving (Read, Show, Eq, Gen.Data, Gen.Typeable) + deriving (Read, Show, Eq, Ord, Gen.Data, Gen.Typeable) hunk ./ParseSyntax.hs 234 - deriving (Read, Show, Eq, Gen.Data, Gen.Typeable) + deriving (Read, Show, Eq, Ord, Gen.Data, Gen.Typeable) hunk ./ParseSyntax.hs 394 + + -- only used internally + | Error String -- indicates a internal error (such as a + -- type-mismatch at runtime) + + | Overloading Overloading -- for overloading resolution hunk ./ParseSyntax.hs 416 +data Overloading = {- Placeholder for a class constraint. Printed -} + Placeholder ClassConstraint + + {- `MethodPlaceholder C m [t1, ..., tN]' represents a call of + method `m' in class `C'. The types specify which instance + of C should be selected. Printed -} + | MethodPlaceholder ClassId ValId [Type] + + | DictionaryReference ClassId [Type] -- dict-C + | DictionaryLookup ValId Exp -- bar@(dict-expr) + | Dictionary [(ValId, Exp)] + deriving (Read,Show,Eq, Gen.Data, Gen.Typeable) + hunk ./ParseSyntax.hs 574 - pprPrec _ (Con tag es) = ppr tag <+> hsep (map ppr es) + pprPrec prec (Con id []) = ppr id + pprPrec prec (Con id es) = + pprPrec prec (foldl App (Con id []) es) hunk ./ParseSyntax.hs 600 - char '\\' <> (hsep (map ppr xs)) <->> ppr e + if not (null xs) then char '\\' <> (hsep (map ppr xs)) <->> ppr e + else pprPrec prec e hunk ./ParseSyntax.hs 620 + pprPrec prec (Overloading o) = pprPrec prec o + +instance Pretty Overloading where + ppr (Placeholder c) = text "<" <> ppr c <> text ">" + ppr (MethodPlaceholder cid mid vars) = + text "<" <> ppr cid <> text "::" <> ppr mid <> text ": " + <> pprList ", " vars <> text ">" + ppr (DictionaryReference cid ts) = + text "dict-" <> ppr cid <> text "<" <> pprList ", " ts <> text ">" + ppr (DictionaryLookup id e) = + ppr id <> text "@" <> parens (ppr e) + ppr (Dictionary l) = + text "{dictionary" $$ + nest 4 (vcat (map (\ (n,e) -> ppr n <> text ":" <+> ppr e) l)) $$ + text "}" hunk ./PhracPrelude.hs 46 - [TyVar "__a", TyVar "__b"]] builtinInfo + [TyVar "__a", TyVar "__b"]] builtinInfo hunk ./PhracPrelude.phc 14 -showInt i = if i == -9 then "-9" else ( - if i == -8 then "-8" else ( - if i == -7 then "-7" else ( - if i == -6 then "-6" else ( - if i == -5 then "-5" else ( - if i == -4 then "-4" else ( - if i == -3 then "-3" else ( - if i == -2 then "-2" else ( - if i == -1 then "-1" else ( - if i == 0 then "0" else ( - if i == 1 then "1" else ( - if i == 2 then "2" else ( - if i == 3 then "3" else ( - if i == 4 then "4" else ( - if i == 5 then "5" else ( - if i == 6 then "6" else ( - if i == 7 then "7" else ( - if i == 8 then "8" else ( - if i == 9 then "9" else ( - let x = i % 10; - y = i / 10; - in showInt y ++ showInt x - ))))))))))))))))))); +showInt __i = if __i == -9 then "-9" else ( + if __i == -8 then "-8" else ( + if __i == -7 then "-7" else ( + if __i == -6 then "-6" else ( + if __i == -5 then "-5" else ( + if __i == -4 then "-4" else ( + if __i == -3 then "-3" else ( + if __i == -2 then "-2" else ( + if __i == -1 then "-1" else ( + if __i == 0 then "0" else ( + if __i == 1 then "1" else ( + if __i == 2 then "2" else ( + if __i == 3 then "3" else ( + if __i == 4 then "4" else ( + if __i == 5 then "5" else ( + if __i == 6 then "6" else ( + if __i == 7 then "7" else ( + if __i == 8 then "8" else ( + if __i == 9 then "9" else ( + let __x = __i % 10; + __y = __i / 10; + in showInt __y ++ showInt __x + ))))))))))))))))))); hunk ./PhracPrelude.phc 43 - show i = showInt i; + show __i = showInt __i; hunk ./PhracPrelude.phc 47 - show c = Cons c Nil; + show __c = Cons __c Nil; +} + +instance Show Bool where { + show __b = case __b of + True -> "True"; + False -> "False"; + ; +} + +instance Show __a => Show (List __a) where { + show l = foldr (\__a __b -> if null __b then show __a + else show __a ++ ", " ++ show __b) "" l; +} + +instance Show __a, Show __b => Show ((__a, __b)) where { + show p = case p of Pair __f __s -> "(" ++ show __f ++ ", " ++ show __s ++ ")";; hunk ./PhracPrelude.phc 78 + +null :: List __a -> Bool; +null __x = case __x of Nil -> True; Cons __y __z -> False;; + +foldr __f __z __l = + case __l of + Nil -> __z; + Cons __x __xs -> __f __x (foldr __f __z __xs); + ; + +length :: List __a -> Int; +length __l = case __l of Nil -> 0; Cons __x __xs -> 1 + (length __xs);; hunk ./Pretty.hs 25 + dumpMap, hunk ./Pretty.hs 43 +import qualified Map hunk ./Pretty.hs 81 + +dumpMap :: (Pretty k, Pretty a) => Map.Map k a -> Doc +dumpMap m = hcat $ + punctuate (text ", ") + (map (\ (k,v) -> ppr k <+> text "-->" <+> ppr v) + (Map.assocs m)) + hunk ./Symtab.hs 35 - findDataConstructor, findMethodSig, getAssocIndexCount, + findDataConstructor, findMethodSig, getAssocIndexCount, isMethod, + getMethods, hunk ./Symtab.hs 38 - instantiate, freshTypeVar, freshTyConstruct, setFreshVarsPrefix + instantiate, freshTypeVar, freshTyConstruct, freshValVar, setFreshVarsPrefix, + + replaceInstances, enterDictionaryExpression, getDictionaryExpressions hunk ./Symtab.hs 45 +import qualified Data.Set as Set hunk ./Symtab.hs 66 - String), -- prefix for type constructors + String, -- prefix for type constructors + String), -- prefix for value variables hunk ./Symtab.hs 69 + methods :: Set.Set ValId, -- which value ids are methods? + dictExprs :: Map.Map (ClassId, [Type]) Exp, hunk ./Symtab.hs 78 - nameSupply = (UniqIdents.initialVersion - 1, "@v", "@c"), + nameSupply = (UniqIdents.initialVersion - 1, "#v", + "#c", "#d"), hunk ./Symtab.hs 81 + methods = Set.empty, + dictExprs = Map.empty, hunk ./Symtab.hs 108 +replaceInstances :: [ClassInst] -> ST () +replaceInstances insts = + do m <- gets classMap + let emptyInsts = Map.map (\ (cdec,_) -> (cdec, [])) m + m' = foldr insertInst emptyInsts insts + modify (\s -> s { classMap = m' }) + where + insertInst :: ClassInst + -> Map.Map ClassId (ClassDec, [ClassInst]) + -> Map.Map ClassId (ClassDec, [ClassInst]) + insertInst ci m = + let cid = inst_class ci in + case Map.lookup cid m of + Nothing -> panic ("Class " ++ showPpr' cid ++ + " not defined") + Just (cdec, l) -> + Map.insert cid (cdec, ci:l) m + hunk ./Symtab.hs 167 +isMethod :: ValId -> ST Bool +isMethod id = + do set <- gets methods + return (Set.member id set) + +getMethods :: ClassId -> ST [ValId] +getMethods cid = + do cdec <- findClass cid + return (map fst (class_vsigs cdec)) + hunk ./Symtab.hs 203 +enterDictionaryExpression :: (ClassId, [Type]) -> Exp -> ST () +enterDictionaryExpression key exp = + do modify (\s -> s { dictExprs = Map.insert key exp (dictExprs s) }) + +getDictionaryExpressions :: ST [((ClassId, [Type]), Exp)] +getDictionaryExpressions = + do m <- gets dictExprs + return $ Map.toList m + hunk ./Symtab.hs 246 -setFreshVarsPrefix :: String -> String -> ST () -setFreshVarsPrefix v c = - do (version, v', c') <- gets nameSupply - if v == v' || c == c' +setFreshVarsPrefix :: String -> String -> String -> ST () +setFreshVarsPrefix v c x = + do (version, v', c', x') <- gets nameSupply + if v == v' || c == c' || x == x' hunk ./Symtab.hs 253 - v, c) }) + v, c, x) }) hunk ./Symtab.hs 256 - do (cur, v, c) <- gets nameSupply - modify (\s -> s { nameSupply = (cur - 1, v, c) }) + do (cur, v, c, x) <- gets nameSupply + modify (\s -> s { nameSupply = (cur - 1, v, c, x) }) hunk ./Symtab.hs 269 - do (cur, v, c) <- gets nameSupply - modify (\s -> s { nameSupply = (cur - 1, v, c) }) + do (cur, v, c, x) <- gets nameSupply + modify (\s -> s { nameSupply = (cur - 1, v, c, x) }) hunk ./Symtab.hs 282 +freshValVar :: ST ValId +freshValVar = + do (cur, v, c, x) <- gets nameSupply + modify (\s -> s { nameSupply = (cur - 1, v, c, x) }) + return $ UniqIdents.mkValId x cur + hunk ./Symtab.hs 314 - show (map (ppr . class_name) (head groups))) + show (map (ppr . class_name) (head cyclic))) hunk ./Symtab.hs 323 - let eqs = mapMaybe toEq (class_tsigs cd) in + let eqs = mapMaybe toEq (class_tsigs cd) + mids = Set.fromList (map fst (class_vsigs cd)) + in hunk ./Symtab.hs 330 - globalEqualities = eqs ++ (globalEqualities s) }) + globalEqualities = eqs ++ (globalEqualities s), + methods = mids `Set.union` (methods s) }) hunk ./SyntaxTransformation.hs 277 - let v = if builtin then "@v" else "v" + let v = if builtin then "#v" else "v" hunk ./TypeInference.hs 1 -module TypeInference where - hunk ./TypeInference.hs 19 + +module TypeInference ( + + tiMain, emptyAssumps, dumpTypeInference + +) where hunk ./TypeInference.hs 32 +import Maybe ( fromJust ) hunk ./TypeInference.hs 45 +import Overloading hunk ./TypeInference.hs 115 + hunk ./TypeInference.hs 118 -type Infer e t = Assumps -> e -> TI ([Constraint], t) +type Infer e t = Assumps -> e -> TI ([Constraint], t, e) hunk ./TypeInference.hs 121 + hunk ./TypeInference.hs 125 - return (ps, t) + 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 hunk ./TypeInference.hs 139 -tiExpr as (Const (Number _)) = return $ ([], TyConstruct intTypeId) -tiExpr as (Const (Character _)) = return $ ([], TyConstruct charTypeId) +tiExpr as e@(Const (Number _)) = + return $ ([], TyConstruct intTypeId, e) +tiExpr as e@(Const (Character _)) = + return $ ([], TyConstruct charTypeId, e) hunk ./TypeInference.hs 146 - let (pss, operandTypes) = unzip l + let (pss, operandTypes, es') = unzip3 l hunk ./TypeInference.hs 151 - return (map EC qs ++ concat pss, alpha) + return (map EC qs ++ concat pss, alpha, Prim op es') hunk ./TypeInference.hs 158 - let (pss, operandTypes) = unzip l + let (pss, operandTypes, es') = unzip3 l hunk ./TypeInference.hs 161 - return (ps ++ map EC qs ++ concat pss, alpha) + return (ps ++ map EC qs ++ concat pss, alpha, Con di es') hunk ./TypeInference.hs 164 - do (ps1, tau1) <- tiExpr as e1 - (ps2, tau2) <- tiExpr as e2 + do (ps1, tau1, e1') <- tiExpr as e1 + (ps2, tau2, e2') <- tiExpr as e2 hunk ./TypeInference.hs 170 - return (mergeConstraints (theta1 ++ theta2) u, alpha) + return (mergeConstraints (theta1 ++ theta2) u, alpha, App e1' e2') hunk ./TypeInference.hs 176 - (ps, tau) <- tiExpr (add x (toScheme alpha) as) (Lam xs e) - return (ps, alpha `tyFun` tau) + let as' = add x (toScheme alpha) as + (ps, tau, e') <- tiExpr as' (Lam xs e) + return (ps, alpha `tyFun` tau, Lam [x] e') hunk ./TypeInference.hs 181 - do (ps1, t1) <- tiExpr as e1 + do (ps1, t1, e1') <- tiExpr as e1 hunk ./TypeInference.hs 184 - (ps2, t2) <- tiExpr as e2 - (ps3, t3) <- tiExpr as e3 + (ps2, t2, e2') <- tiExpr as e2 + (ps3, t3, e3') <- tiExpr as e3 hunk ./TypeInference.hs 188 - return (ps1 ++ ps2 ++ ps3 ++ (map EC $ qs1 ++ qs2 ++ qs3), alpha) + return (ps1 ++ ps2 ++ ps3 ++ (map EC $ qs1 ++ qs2 ++ qs3), + alpha, If e1' e2' e3') hunk ./TypeInference.hs 192 - do (ps, as') <- tiBindGroup NestedLevel as binds - (qs, t) <- tiExpr (as' `merge` as) e - return (ps ++ qs, t) + do (ps, as', binds') <- tiBindGroup NestedLevel as binds + (qs, t, e') <- tiExpr (as' `merge` as) e + return (ps ++ qs, t, Letrec binds' e') hunk ./TypeInference.hs 197 - do (ps, t) <- tiExpr as e + do (ps, t, e') <- tiExpr as e hunk ./TypeInference.hs 203 - let (rss, resTys) = unzip l' + let (rss, resTys, es') = unzip3 l' hunk ./TypeInference.hs 206 + let alts' = map (\ (a,e) -> a { alt_exp = e }) (zip alts es') hunk ./TypeInference.hs 208 - alpha) + alpha, Case e' alts') hunk ./TypeInference.hs 218 - hunk ./TypeInference.hs 219 --- the Bind type here corresponds to the Alt type in THIH -type Bind = ([ValId] {- arguments -} , Exp) hunk ./TypeInference.hs 225 - (qs, t) <- tiExpr (as' `merge` as) e + (qs, t, e') <- tiExpr (as' `merge` as) e hunk ./TypeInference.hs 227 - return (qs, resTy) - - -subsumes :: TypeScheme -> TypeScheme -> TI Bool -subsumes sc1@(TypeScheme quants1 (QualifiedType pi1 tau1)) - 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 - 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 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 + return (qs, resTy, (is, e')) hunk ./TypeInference.hs 233 -tiExpl :: Assumps -> Expl -> TI [Constraint] -tiExpl as (i, sc, bind) = +tiExpl :: Assumps -> Expl -> TI ([Constraint], Expl) +tiExpl as (i, sc@(TypeScheme _ (QualifiedType qs _)), bind) = hunk ./TypeInference.hs 236 - -- not pass the subsumption check, although the look like they should + -- not pass the subsumption check, although they look like they should hunk ./TypeInference.hs 239 - debug (dumpAssumps as) - (ps, t) <- tiBind as bind -- infered type + (ps, t, bind') <- tiBind as bind -- infered type hunk ./TypeInference.hs 242 - ps' = applySubst s ps - fs = freeTypeVars (applySubst s as) - -- we must simplify the infered constraints by filtering out those - -- constraints which contain only fixed variables (i.e. variables - -- appearing in the assumptions). Such contraints are deferred - -- to the enclosing bindings. - (ds, ps'') = partition (all (`Set.member` fs) . freeTypeVarsList) ps' - gs = (freeTypeVars ps'' `Set.union` freeTypeVars t') + ps' = applySubst s ps + as' = applySubst s as + fs = freeTypeVars as' + gs = (freeTypeVars ps' `Set.union` freeTypeVars t') hunk ./TypeInference.hs 247 - sc' = TypeScheme (Set.toList gs) (QualifiedType ps'' t') + (ds, ps'') <- liftST $ split (Set.toList fs) (Set.toList gs) ps' + sc' <- generalize i (Set.toList gs) ps'' t' hunk ./TypeInference.hs 250 - ", new checking for subsumption\n--------") - b <- subsumes sc' sc - if not b - then phasefail ("type error while checking explicitly typed binding " - ++ showPpr' i ++ "\n infered signature: " - ++ showPpr sc' ++ "\n user-supplied signature: " - ++ showPpr sc) - else do debug ("Finished typing explicitly typed binding " ++ - showPpr' i ++ " deferred constraints: " ++ - showCommaListed ds ++ "\n\n" ++ showTypeSig (i,sc) - ++ "\n\n") - return ds - + ", new 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 debug ("Finished typing explicitly typed binding " ++ + showPpr' i ++ " deferred constraints: " ++ + showCommaListed ds ++ "\n\n" ++ showTypeSig (i,sc) + ++ "\n\n") + -- 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'' + 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 = panic ("unexpected Overload value: " ++ showPpr' o) hunk ./TypeInference.hs 289 - debug (dumpAssumps as) hunk ./TypeInference.hs 294 - let (pss, types) = unzip l + let (pss, types, bs') = unzip3 l hunk ./TypeInference.hs 300 - fs = freeTypeVars (applySubst s as) + as' = applySubst s as + fs = freeTypeVars as' hunk ./TypeInference.hs 312 - (constrs, scs') <- + (constrs, scs', bs'') <- hunk ./TypeInference.hs 315 - let gs' = gs `Set.difference` (freeTypeVars rs) - scs'' = map (\t -> TypeScheme (Set.toList gs') - (QualifiedType [] t)) ts' - in do debug ("The monomorphism restriction applies") - return (ds ++ rs, scs'') + 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''') hunk ./TypeInference.hs 323 - let scs'' = map (\t -> TypeScheme (Set.toList gs) - (QualifiedType rs t)) ts' - in do debug ("The monomorphism restriction does not apply") - return (ds, scs'') + 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''') hunk ./TypeInference.hs 331 + resImpls = zip is bs'' hunk ./TypeInference.hs 334 - return (constrs, resAssumps) + return (constrs, resAssumps, resImpls) hunk ./TypeInference.hs 356 -tiImplsSeq _ as [] = return ([], emptyAssumps) +tiImplsSeq _ as [] = return ([], emptyAssumps, []) hunk ./TypeInference.hs 358 - do (ps, as') <- tiImpls level as bs - (qs, as'') <- tiImplsSeq level (as' `merge` as) bss - return (ps ++ qs, as'' `merge` as') + 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') hunk ./TypeInference.hs 370 - (ps, as'') <- tiImplsSeq level (as' `merge` as) (splitImpls impls) + (ps, as'', impls') <- tiImplsSeq level (as' `merge` as) + (splitImpls impls) hunk ./TypeInference.hs 375 - qss <- mapM (tiExpl (as'' `merge` as' `merge` as)) expls + l <- mapM (tiExpl (as'' `merge` as' `merge` as)) expls + let (qss, expls') = unzip l hunk ./TypeInference.hs 379 - mapM checkForAmbiguity (Map.assocs resAssumps) + resBinds = reconstructValBinds binds impls' expls' hunk ./TypeInference.hs 384 - return (resConstrs, resAssumps) + return (resConstrs, resAssumps, resBinds) hunk ./TypeInference.hs 393 - -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) - || - -- 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 () + reconstructValBinds :: [ValBind] -> [[Impl]] -> [Expl] -> [ValBind] + reconstructValBinds origBinds impls expls = + let bs = concat impls ++ (map (\ (i, sc, b) -> (i, b)) expls) + replExp vb = + let (params, e) = fromJust (lookup (vbind_name vb) bs) + in vb { vbind_exp = e, vbind_params = params } + in map replExp origBinds + hunk ./TypeInference.hs 402 -tiMain :: Assumps -> Program -> ST Assumps -tiMain initAs (Program _ classes instances valBinds) = - do (ps, as) <- runTI $ ti classes instances valBinds +tiMain :: Assumps -> Program -> ST (Assumps, Program) +tiMain initAs prog@(Program _ classes instances valBinds) = + do (ps, as, valBinds', instances') <- runTI $ ti classes instances valBinds hunk ./TypeInference.hs 409 - return normed + return (normed, prog { prog_bindings = valBinds', + prog_instances = instances' }) hunk ./TypeInference.hs 417 - (ps, as') <- tiBindGroup TopLevel as binds + (ps, as', binds') <- tiBindGroup TopLevel as binds hunk ./TypeInference.hs 419 - -- check the types of the methods - mapM (checkMethods as'') instances + -- check the types of the methods and resolve overloading + instances' <- mapM (checkMethods as'') instances hunk ./TypeInference.hs 422 - return (applySubst s ps, applySubst s as'') + return (applySubst s ps, applySubst s as'', binds', instances') hunk ./TypeInference.hs 435 - checkMethods :: Assumps -> ClassInst -> TI () + checkMethods :: Assumps -> ClassInst -> TI ClassInst hunk ./TypeInference.hs 439 - mapM_ (checkMethod as ci) (inst_valBinds ci) - checkMethod :: Assumps -> ClassInst -> ValBind -> TI () - checkMethod as ci (ValBind i _ params e _) = + binds <- mapM (checkMethod as ci) (inst_valBinds ci) + return (ci { inst_valBinds = binds }) + checkMethod :: Assumps -> ClassInst -> ValBind -> TI ValBind + checkMethod as ci bind@(ValBind i _ params e _) = hunk ./TypeInference.hs 448 - let cs' = List.nub (inst_constraints ci ++ cs) + let cs' = inst_constraints ci ++ cs hunk ./TypeInference.hs 457 - ps <- tiExpl as (i, sc', (params, e)) + (ps, (_, _, (params', e'))) <- tiExpl as (i, sc', (params, e)) + let bind' = bind { vbind_params = params', + vbind_exp = e' } hunk ./TypeInference.hs 464 - else return () + else do debug ("resolved overloading for method " ++ + showPpr' i ++ ": " ++ showPpr' bind') + return bind' hunk ./TypeInference.hs 475 + + +-- 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') -> + 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)) = + let fv_rho = freeTypeVars rho + fixv_rho = fixedTypeVars rho + in 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 () + hunk ./Unification.hs 26 - matchType, matchTypes, normalise, + matchType, matchTypes, matchConstraint, normalise, hunk ./Unification.hs 48 + +-- `matchConstraint (A, ts) c' checks if the constraint c is fulfilled +-- by the instance declaration A ts. +matchConstraint :: (ClassId, [Type]) -> ClassConstraint -> ST (Maybe TypeSubst) +matchConstraint (id, ts) (ClassConstraint id' ts') + | id /= id' + = return Nothing + | otherwise + = do -- first normalize the type + tns <- runUF [] (mapM normalise ts) + tns' <- runUF [] (mapM normalise ts') + -- then use match to see if there is a substitution s such that + -- applySubst s t = t' + matchTypes tns tns' hunk ./UniqIdents.hs 45 - mkTypeVar, mkTypeId + mkTypeVar, mkTypeId, mkValId hunk ./UniqIdents.hs 313 +mkValId :: String -> Version -> ValId +mkValId s v = + if v >= initialVersion + then panic ("mkValId called with illegal version number: " ++ + show v) + else (ValId (Id v s)) addfile ./tests/overloading-resolution/should_pass/000.out hunk ./tests/overloading-resolution/should_pass/000.out 1 +f :: forall v[-5] . Num v[-5] => v[-5] -> v[-5] +f d[-7] x = add@(d[-7]) x (f d[-7] x) addfile ./tests/overloading-resolution/should_pass/000.phc hunk ./tests/overloading-resolution/should_pass/000.phc 1 +class Num a where { + add :: a -> a -> a; +} + +f x = add x (f x); addfile ./tests/overloading-resolution/should_pass/001.out hunk ./tests/overloading-resolution/should_pass/001.out 1 +g :: forall v[-7] . Show v[-7] => List v[-7] -> List Char +g d[-10] x = show@(dict-Show<(__a[6], __b[4])> (dict-Show d[-10]) dict-Show) (Pair x (length x)) addfile ./tests/overloading-resolution/should_pass/001.phc hunk ./tests/overloading-resolution/should_pass/001.phc 1 +g x = show (x, length x); addfile ./tests/overloading-resolution/should_pass/002.out hunk ./tests/overloading-resolution/should_pass/002.out 1 +f :: forall v[-2] . Y v[-2] => v[-2] -> Int +dict-C: +\d[-24] -> {dictionary + cfoo: (\d[-20] x[1] y -> yfoo@(d[-20]) x[1] + xfoo@(dict-X) x[1] + y) d[-24] + xfoo: xfoo@(dict-X) + } +dict-X: +{dictionary + xfoo: \x -> 42 +} +f d[-7] x[2] = cfoo@(dict-C d[-7]) x[2] 42 addfile ./tests/overloading-resolution/should_pass/002.phc hunk ./tests/overloading-resolution/should_pass/002.phc 1 +class X a b where { + xfoo :: a -> b; +} + +class X a b => C a b where { + cfoo :: a -> b -> b; +} + +class Y a where { + yfoo :: a -> Int; +} + +instance X a Int where { + xfoo x = 42; +} + +instance Y a => C a Int where { + cfoo x y = yfoo x + xfoo x + y; +} + + +f x = cfoo x 42; addfile ./tests/overloading-resolution/should_pass/003.out hunk ./tests/overloading-resolution/should_pass/003.out 1 +bar :: forall v[-5] v[-2] . X v[-2], C v[-5] => v[-2] -> v[-5] +dict-C: +{dictionary + foo: \d[-12] x -> getInt@(d[-12]) x +} +bar d[-6] d[-7] x[1] = foo@(d[-7]) d[-6] x[1] addfile ./tests/overloading-resolution/should_pass/003.phc hunk ./tests/overloading-resolution/should_pass/003.phc 1 +class X a where { + getInt :: a -> Int; +} + +class C a where { + foo :: X b => b -> a; +} + +instance C Int where { + foo x = getInt x; +} + +bar x = foo x; addfile ./tests/overloading-resolution/should_pass/004.out hunk ./tests/overloading-resolution/should_pass/004.out 1 +dict-X: +\d[-10] -> {dictionary + foo: (\d[-5] d[-6] x -> undefined) d[-10] + } addfile ./tests/overloading-resolution/should_pass/004.phc hunk ./tests/overloading-resolution/should_pass/004.phc 1 +data D t = D t; + +class C1 a where { + bar1 :: a; +} + +class C2 a where { + bar2 :: a; +} + +class X a where { + foo :: C2 b => b -> a; +} + +instance C1 a => X (D a) where { + foo x = undefined; +} + +-- dict-X: +-- +-- \d_C1 -> [("foo", (\d_C1' -> \d_C2 -> undefined) d_C1)] +-- addfile ./tests/overloading-resolution/should_pass/005.out hunk ./tests/overloading-resolution/should_pass/005.out 1 +dict-C: +{dictionary + bar: undefined + foo: foo@(dict-S dict-S) +} +dict-S: +\d[-8] -> {dictionary + foo: (\d[-3] -> undefined) d[-8] + } +dict-S: +{dictionary + foo: 1 +} addfile ./tests/overloading-resolution/should_pass/005.phc hunk ./tests/overloading-resolution/should_pass/005.phc 1 +class S a where { + foo :: a; +} + +class S a => C a where { + bar :: a; +} + +instance S Int where { + foo = 1; +} + +instance S a => S (List a) where { + foo = undefined; +} + +instance C (List Int) where { + bar = undefined; +} + +-- dict-S: +-- +-- [("foo", 1)] + +-- dict-S: +-- +-- \d_S -> [("foo", (\d_S' -> undefined) d_S)] + +-- dict-C: +-- +-- [("bar", undefined), +-- ("foo", foo@(dict-S dict-S))] addfile ./tests/overloading-resolution/should_pass/006.out hunk ./tests/overloading-resolution/should_pass/006.out 1 +dict-C: +{dictionary + foo: \i -> bar@(dict-C) i + bar: \i[1] -> foo@(dict-C) i[1] +} addfile ./tests/overloading-resolution/should_pass/006.phc hunk ./tests/overloading-resolution/should_pass/006.phc 1 +class C a where { + foo :: a -> Int; + bar :: Int -> a; +} + +instance C Int where { + foo i = bar i; + bar i = foo i; +} addfile ./tests/overloading-resolution/should_pass/Flag hunk ./tests/overloading-resolution/should_pass/Flag 1 +--dump-over --dump-infer hunk ./tests/type-inference/should_fail/003.err 2 - infered signature: forall v[-3] . C v[-3], T v[-3] = Bool => v[-3] -> Int + infered signature: forall v[-4] . T v[-4] = Bool, C v[-4] => v[-4] -> Int hunk ./tests/type-inference/should_fail/008.err 2 - infered signature: forall v[-3] . T v[-3] = Int, C v[-3] => v[-3] -> Int + infered signature: forall v[-4] . C v[-4], T v[-4] = Int => v[-4] -> Int hunk ./tests/type-inference/should_fail/015.err 1 -Cannot unify {v[-22] -> Int = E Int -> v[-27], T v[-22] = Int}. Unsatisfiable equality constraint: Bool = Int +Cannot unify {v[-23] -> Int = E Int -> v[-28], T v[-23] = Int}. Unsatisfiable equality constraint: Bool = Int }