[improved type inference, tests
mail@stefanwehr.de**20050522091009] {
adddir ./tests/type-inference
adddir ./tests/type-inference/should_fail
adddir ./tests/type-inference/should_pass
hunk ./Entailment.hs 126
-    do ps' <- reduce ps
+    do debug ("splitting constraints " ++ showCommaListed ps ++ 
+              ". fixed variables: " ++ showCommaListed fs ++
+              ". variables selected for quantification: " ++ showCommaListed gs)
+       ps' <- reduce ps
hunk ./Entailment.hs 131
+       debug ("splitting finished, deferred constraints: " ++ 
+              showCommaListed ds ++ ", retained constraints: " ++
+              showCommaListed rs)
hunk ./Error.hs 23
-    phasefail_, panic_, failwith_,
+    phasefail_, panic_, 
hunk ./Error.hs 27
-    FailureCause(..),
-    catchFailure, mkCatchFailure,
hunk ./Error.hs 47
-data FailureCause 
-    = PhaseFailed
-    | Panic
-    | UnificationFailed
-    | ReductionFailed
-    | MatchingFailed
-      deriving (Eq,Show)
-
-data PException = PException FailureCause Location String
-      deriving Eq  
+data PException
+    = PhaseFailed Location String -- name of phase, message
+    | Panic Location String       -- the `impossible' happened
+  deriving Eq
hunk ./Error.hs 56
-showPException (PException cause (fname, lineno) msg)
-    = fname  ++ ":" ++ show lineno ++ ": " ++ 
-      show cause ++ "\n\t" ++ msg
+showPException (PhaseFailed (fname, lineno) msg)
+    = fname  ++ ":" ++ show lineno ++ ": " ++ msg
+showPException (Panic (fname, lineno) msg)
+    = fname  ++ ":" ++ show lineno ++ ": PANIC!\n\t" ++ msg
hunk ./Error.hs 62
-showWithoutLocation (PException cause _ msg)
-    = show cause ++ ":\n\t" ++ msg
+showWithoutLocation (PhaseFailed (fname, lineno) msg) = msg
+showWithoutLocation (Panic (fname, lineno) msg) 
+    = fname  ++ ":" ++ show lineno ++ ": PANIC!\n\t" ++ msg
hunk ./Error.hs 77
-catchFailure :: IO a -> [FailureCause] -> (PException -> IO a) -> IO a
-catchFailure io causes handler = 
-    E.catchDyn io h
-    where h e@(PException cause loc msg) = 
-              if cause `elem` causes then handler e
-              else E.throwDyn e
-              
---mkCatch :: ST a -> [FailureCause] -> (FailureCause -> ST a) -> ST a
-mkCatchFailure catch m causes handler = 
-    do state <- get
-       (state', res) <- lift $ catch (evalStateT (patch m) state)
-                               causes 
-                               (\c -> evalStateT (patch (handler c)) state)
-       put state
-       return res
-    where --patch :: ST a -> ST (Symtab, a)
-          patch m = do a <- m
-                       state <- get
-                       return (state, a)
hunk ./Error.hs 82
-panic_ l  x = E.throwDyn (PException Panic l x)
+panic_ l  x = E.throwDyn (Panic l x)
hunk ./Error.hs 85
-phasefail_ l x = E.throwDyn (PException PhaseFailed l x)
-
-failwith_ :: Location -> FailureCause -> String -> a
-failwith_ l c x = E.throwDyn (PException c l x)
+phasefail_ l x = E.throwDyn (PhaseFailed l x)
hunk ./KindInference.hs 280
--- kind inference proper
hunk ./KindInference.hs 284
-     runKI $ do --mapM insertBuiltin Builtins.typeConstructors
-                mapM kiGroup groups
+     runKI $ do mapM kiGroup groups
hunk ./Main.hs 72
-               tiMain ast
+               tyEnv <- tiMain ast
+               when (on $ Dump TypeInfer) $
+                    do liftIO $ dump (dumpTypeInference tyEnv ast)
+               return ()
hunk ./Main.hs 77
-
-dump :: Doc -> IO ()
-dump p = do hPutStrLn stdout (show p)
+dump :: Pretty p => p -> IO ()
+dump p = do hPutStrLn stdout (showPpr p)
hunk ./Main.hs 85
-    (flags,files) <- parseArgs args prog
+    (flags',files) <- parseArgs args prog
hunk ./Main.hs 87
+    let flags = Dump TypeInfer : flags' -- for now...
+
hunk ./Main.hs 96
-        hPutStrLn stderr ""
hunk ./Main.hs 99
-        hPutStrLn stderr ""
hunk ./Main.hs 168
-    | Infer
-    | RawInfer
-    | Final
-    | RawFinal
-    | Haskell
+    | TypeInfer
+--    | RawInfer
+--    | Final
+--    | RawFinal
+--    | Haskell
hunk ./Main.hs 195
-    , Option []    ["dump-infer"]   (NoArg (Dump Infer)) 
-            "print syntax after type inference"
-    , Option []    ["dump-rawinfer"]   (NoArg (Dump RawInfer)) 
-            "print data type after type inference"
-    , Option []    ["dump-final"]  (NoArg (Dump Final)) 
-            "print final syntax, after type checking"
-    , Option []    ["dump-rawfinal"]  (NoArg (Dump RawFinal)) 
-            "print final data type, after type checking"
-    , Option []    ["dump-haskell"] (NoArg (Dump Haskell)) 
-            "print generated haskell"
+    , Option []    ["dump-infer"]   (NoArg (Dump TypeInfer)) 
+            "print types after type inference"
+--    , Option []    ["dump-rawinfer"]   (NoArg (Dump RawInfer)) 
+--            "print data type after type inference"
+--    , Option []    ["dump-final"]  (NoArg (Dump Final)) 
+--            "print final syntax, after type checking"
+--    , Option []    ["dump-rawfinal"]  (NoArg (Dump RawFinal)) 
+--            "print final data type, after type checking"
+--    , Option []    ["dump-haskell"] (NoArg (Dump Haskell)) 
+--            "print generated haskell"
hunk ./Main.hs 207
-    , Option ['H'] ["haskell"]     (NoArg ViaHaskell) "compile to Haskell"
+--    , Option ['H'] ["haskell"]     (NoArg ViaHaskell) "compile to Haskell"
hunk ./ParseSyntax.hs 140
-mergeConstraints :: ([ClassConstraint], [EqConstraint]) -> [Constraint]
-mergeConstraints (cs,es) = 
+mergeConstraints :: [ClassConstraint] -> [EqConstraint] -> [Constraint]
+mergeConstraints cs es = 
hunk ./ParseSyntax.hs 396
-        pprInfixOp prec qualifiedTypeSpec
-          (punctuate (char ',') (map ppr constrs))
-          (space <> text "=>" <> space)
-          ty
+        if not (null constrs)
+           then pprInfixOp prec qualifiedTypeSpec
+                    (pprList ", " constrs)
+                    (space <> text "=>" <> space)
+                    ty
+           else pprPrec prec ty
hunk ./ParseSyntax.hs 410
-                  (text "forall" <+> ppr vars) 
+                  (text "forall" <+> pprList " " vars) 
hunk ./Parser.y 213
-    | 'letrec' valBinds 'in' exp        { Let (reverse $2) $4     }
+    | 'letrec' valBinds 'in' exp        { Letrec (reverse $2) $4     }
hunk ./ParserHelper.hs 17
-            TypeDef "->" ["1", "2"] [],
+            TypeDef "->" ["a", "b"] [],
hunk ./ParserHelper.hs 19
-            TypeDef "(,)" ["3", "4"] [DataConstructor "Pair"
-                                      [TyVar "3", TyVar "4"]]]
+            TypeDef "(,)" ["a", "b"] [DataConstructor "Pair"
+                                      [TyVar "a", TyVar "b"]]]
hunk ./Pretty.hs 23
-    printDoc, showPpr, showPpr', showList, showCommaListed,
+    printDoc, showPpr, showPpr', showList, showCommaListed, pprList,
hunk ./Pretty.hs 25
-    -- helper
hunk ./Pretty.hs 61
-        parens `usedWhen` (prec > minPrec) $ hsep (map (pprPrec maxPrec) s)
+        parens `usedWhen` (prec > minPrec) $ hcat (map (pprPrec maxPrec) s)
hunk ./Substitution.hs 45
-    (concat . intersperse ", ") 
-    (map (\ (v,t) -> showPpr v ++ " -> " ++ showPpr t) s)
+    (concat . intersperse ", ")
+    (map (\ (v,t) -> showPpr v ++ " |--> " ++ showPpr t) s)
hunk ./Symtab.hs 8
-  ST, liftIO, runST, catchST,
+  ST, liftIO, runST,
hunk ./Symtab.hs 13
-  findTypeDef, getEqEnv, findSuperClasses,
+  findTypeDef, getEqEnv, findSuperClasses, findDataConstructor,
hunk ./Symtab.hs 53
-catchST :: ST a -> [FailureCause] -> (PException -> ST a) -> ST a
-catchST st causes handler = mkCatchFailure catchFailure st causes handler
-
hunk ./Symtab.hs 93
+findDataConstructor :: DataId -> ST (TypeDef, DataConstructor)
+findDataConstructor id = 
+    do tab <- gets typeDefMap
+       return $ find id (Map.elems tab)
+   where find id [] = phasefail ("unknown data constructor: " ++ showPpr' id)
+         find id (x:xs) = 
+             case List.find ((==) id . dconstr_name) (tydef_alts x) of
+               Just dcons -> (x, dcons)
+               Nothing -> find id xs
+
hunk ./Symtab.hs 201
-        do --insertBuiltins
-           mapM insertTypeDef typeDefs
+        do mapM insertTypeDef typeDefs
hunk ./SyntaxTransformation.hs 266
-rwExp (Con tg _) = 
-    panic "parser should not produce constructor expression with non-empty \
-           \expression list"
+rwExp (Con tg args) = 
+  do (tg', arity) <- lookUpDataCon tg
+     if arity /= length args
+        then panic ("arity mismatch in constructor expression with " ++
+                    "non-empty argument list")
+        else do args' <- mapM rwExp args
+                return $ AS.Con tg' args'
hunk ./TypeInference.hs 7
+import List (partition, intersperse)
+import qualified Data.Generics as Gen
+
hunk ./TypeInference.hs 21
+import DependAnalysis
hunk ./TypeInference.hs 93
-type Infer e t = Assumps -> e -> TI (([ClassConstraint], [EqConstraint]), t)
+type Infer e t = Assumps -> e -> TI ([Constraint], t)
hunk ./TypeInference.hs 99
-       return (splitConstraints ps, t)
+       return (ps, t)
hunk ./TypeInference.hs 101
-tiExpr as (Num _) = return $ (([], []), TyConstruct intTypeId)
+tiExpr as (Num _) = return $ ([], TyConstruct intTypeId)
hunk ./TypeInference.hs 105
+       let (pss, operandTypes) = unzip l
hunk ./TypeInference.hs 107
-       let (constrs, operandTypes) = unzip l
-           opTy = typeOfPrimOp op
+       let opTy = typeOfPrimOp op
hunk ./TypeInference.hs 109
-       unify [] opTy resTy
-       return (unzipConstraints constrs, alpha)
+       qs <- unify [] opTy resTy
+       return (map EC qs ++ concat pss, alpha)
hunk ./TypeInference.hs 112
+tiExpr as (Con di es) =
+    do (tydef, dataCons) <- liftST $ findDataConstructor di
+       let quants = tydef_params tydef
+           tc = TyConstruct (tydef_name tydef)
+           resTy = foldl TyApp tc (map TyVar quants)
+       (ty,_ ) <- liftST $ instantiate quants (tyFuns (dconstr_params dataCons)
+                                               resTy)
+       alpha <- liftST $ freshTypeVar KindStar
+       l <- mapM (tiExpr as) es
+       let (pss, operandTypes) = unzip l
+           ty' =  tyFuns operandTypes alpha
+       qs <- unify [] ty ty'
+       return (map EC qs ++ concat pss, alpha)
+
hunk ./TypeInference.hs 127
-    do ((theta1, u1), tau1) <- tiExpr as e1
-       ((theta2, u2), tau2) <- tiExpr as e2
+    do (ps1, tau1) <- tiExpr as e1
+       (ps2, tau2) <- tiExpr as e2
+       let (theta1, u1) = splitConstraints ps1
+           (theta2, u2) = splitConstraints ps2
hunk ./TypeInference.hs 133
-       return ((theta1 ++ theta2, u), alpha)
+       return (mergeConstraints (theta1 ++ theta2) u, alpha)
hunk ./TypeInference.hs 142
+tiExpr as (If e1 e2 e3) = 
+    do (ps1, t1) <- tiExpr as e1
+       qs1 <- unify [] t1 boolType
+       alpha <- liftST $ freshTypeVar KindStar
+       (ps2, t2) <- tiExpr as e2
+       (ps3, t3) <- tiExpr as e3
+       qs2 <- unify [] t2 alpha
+       qs3 <- unify [] t3 alpha
+       return (ps1 ++ ps2 ++ ps3 ++ (map EC $ qs1 ++ qs2 ++ qs3), alpha)
+
hunk ./TypeInference.hs 153
-    do ((ps, psEq), as') <- tiBindGroup as binds
-       ((qs, qsEq), t) <- tiExpr (as' `merge` as) e
-       return ((ps ++ qs, psEq ++ qsEq), t)
+    do (ps, as') <- tiBindGroup as binds
+       (qs, t) <- tiExpr (as' `merge` as) e
+       return (ps ++ qs, t)
hunk ./TypeInference.hs 157
+tiExpr as e = 
+    do panic ("tiExpr for " ++ showPpr' e ++ " not yet implemented")
+
hunk ./TypeInference.hs 210
-tiExpl :: Assumps -> Expl -> TI ([ClassConstraint], [EqConstraint])
+tiExpl :: Assumps -> Expl -> TI [Constraint]
hunk ./TypeInference.hs 212
-    do (ps, t) <- tiBind as bind  -- infered type
-       (qs, x) <- freshInst sc    -- user supplied type
-       unify [] t x               -- important 
+    do debug ("typing explicitly type binding " ++ showPpr' i ++ "\n")
+       (ps, t) <- tiBind as bind  -- infered type
hunk ./TypeInference.hs 216
-           ps' = mergeConstraints $ applySubst s ps 
+           ps' = applySubst s ps 
hunk ./TypeInference.hs 218
-           gs = (freeTypeVars ps' `Set.union` freeTypeVars t')
+           -- 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')
hunk ./TypeInference.hs 227
-                  else ConstrainedType ps' t')
+                  else ConstrainedType ps'' t')
+       debug ("type infered for " ++ showPpr' i ++ ": " ++ showPpr sc' ++
+             ", new checking for subsumption\n--------")
hunk ./TypeInference.hs 232
-          then phasefail ("type error while checking explicitly typed binding `"
-                          ++ showPpr i ++ "': user-supplied signature too " ++
-                          "general\n  infered signature: " 
+          then phasefail ("type error while checking explicitly typed binding "
+                          ++ showPpr' i ++ "\n  infered signature: " 
hunk ./TypeInference.hs 236
-          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
+          else do debug ("Finished typing explicitly typed binding " ++ 
+                         showPpr' i ++ " deferred constraints: " ++ 
+                         showCommaListed ds ++ "\n\n" ++ showTypeSig (i,sc)
+                         ++ "\n\n")
+                  return ds
hunk ./TypeInference.hs 248
-    do -- type for every bindind
+    do let is = map fst bs
+       debug ("typing implicitly typed bindings " ++ showCommaListed is)
+       -- type for every bindind
hunk ./TypeInference.hs 252
-       let is = map fst bs
-           scs = map toScheme ts
+       let scs = map toScheme ts
hunk ./TypeInference.hs 255
-       let (constrs, types) = unzip l
-           ps = mergeConstraints (unzipConstraints constrs)
-       mapM (uncurry $ unify []) (zip ts types)
+       let (pss, types) = unzip l
+           ps = concat pss
+       -- FIXME: use result of unify.
+       qss <- mapM (uncurry $ unify []) (zip ts types) 
+       if not (null $ concat qss) 
+          -- TRY TO FIND A TESTCASE WHICH BREAKS THIS!!
+          then panic "tiImpls: FIXME"
+          else return ()
hunk ./TypeInference.hs 269
+       debug ("monotypes for implicitly type bindings: " ++
+              showCommaListed (map (\ (i, t) -> ppr i <+> text " :: " <+> 
+                                                ppr t) (zip is ts')) ++ 
+              ", constraints: " ++ showCommaListed ps')
hunk ./TypeInference.hs 276
-       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')
+       (constrs, scs') <-
+           if restricted bs 
+              then
+              let gs' = gs `Set.difference` (freeTypeVars rs)
+                  scs'' = map (\t -> TypeScheme (Set.toList gs')
+                                       (UnconstrainedType t)) ts'
+              in do debug ("The monomorphism restriction applies")
+                    return (ds ++ rs, scs'')
+              else
+              let scs'' = map (\t -> TypeScheme (Set.toList gs) 
+                                       (ConstrainedType rs t)) ts'
+              in do debug ("The monomorphism restriction does not apply")
+                    return (ds, scs'')
+       let resAssumps = buildAssumps is scs'
+       debug ("finished typing implicitly typed bindings, deferred " ++
+              "constraints: " ++ showCommaListed constrs ++ "\n\n" ++
+               (showTypeSigs (Map.assocs resAssumps)) ++ "\n\n")
+       return (constrs, resAssumps)
hunk ./TypeInference.hs 299
-       
+    
+   
+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 _ = []
hunk ./TypeInference.hs 314
+tiImplsSeq :: Infer [[Impl]] Assumps
+tiImplsSeq as [] = return ([], emptyAssumps)
+tiImplsSeq as (bs:bss) = 
+    do (ps, as') <- tiImpls as bs
+       (qs, as'') <- tiImplsSeq (as' `merge` as) bss
+       return (ps ++ qs, as'' `merge` as')
hunk ./TypeInference.hs 321
--- FIXME: need depend analysis
hunk ./TypeInference.hs 323
-    do let (as', expls, impls) = collect emptyAssumps binds
-       (ps, as'') <- tiImpls (as' `merge` as) impls
+    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'') <- tiImplsSeq (as' `merge` as) (splitImpls impls)
+       debug ("assumptions obtained by typing the implicitly typed bindings: "
+              ++ dumpAssumps as'' ++ ", constraints: " ++ 
+              showCommaListed ps)
hunk ./TypeInference.hs 334
-       let resConstrs = unzipConstraints qss
+       let resConstrs = concat qss ++ ps
hunk ./TypeInference.hs 337
+       debug ("finished typing binding group " ++ showCommaListed ids ++
+              ", resulting assumptions: " ++ dumpAssumps resAssumps ++ 
+              ", resulting constraints: " 
+              ++ showCommaListed resConstrs)
hunk ./TypeInference.hs 344
-    collect _ (ValBind id Nothing params e : rest) =
+    collect as (ValBind id Nothing params e : rest) =
hunk ./TypeInference.hs 361
-tiMain :: Program -> ST ()
+tiMain :: Program -> ST Assumps
hunk ./TypeInference.hs 363
-    do ((cs,es), as) <- runTI $ ti emptyAssumps valBinds
-       liftIO $ putStrLn (dumpAssumps as)
-       liftIO $ putStrLn (dumpClassConstraints cs)
-       liftIO $ putStrLn (dumpEqConstraints es)
-       return ()
+    do debug "\n\n  ==> STARTING TYPE INFERENCE <== \n\n"
+       (ps, as) <- runTI $ ti emptyAssumps valBinds
+       if not (null ps)
+          then panic ("Non-empty set of constraints after type inference:\n" ++
+                      dumpAssumps as ++ "\n" ++ dumpConstraints ps)
+          else return as
hunk ./TypeInference.hs 429
+dumpTypeInference :: Assumps -> Program -> String
+dumpTypeInference as (Program _ classes _ binds) =
+    let methods = concatMap dumpMethods classes
+        values = map dumpValue binds
+    in concat (intersperse "\n" $ methods ++ values)
+    where
+    dumpMethods :: ClassDec -> [String]
+    dumpMethods cd = [] -- FIXME map dump (class_tsigs cd)
+    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)
hunk ./TypeInference.hs.old 6
+import qualified Data.Set as Set
+import List (partition, intersperse)
+
+import qualified Builtins
+import UniqIdents ( builtinTypeId )
+import Builtins
hunk ./TypeInference.hs.old 17
+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'
hunk ./TypeInference.hs.old 42
-type InstanceEnv = [ConstraintScheme]
-type TypeEnv = Map.Map ValId TypeScheme
+buildAssumps :: [ValId] -> [TypeScheme] -> Assumps
+buildAssumps is ts = Map.fromList (zip is ts)
hunk ./TypeInference.hs.old 45
-lookupTyEnv :: ValId -> TypeEnv -> Maybe TypeScheme
-lookupTyEnv = Map.lookup
+dumpAssumps :: Assumps -> String
+dumpAssumps as = 
+    "{Assumptions: " ++
+    showCommaListed (map (\ (k,v) -> ppr k <+> text "=" <+> ppr v)
+                     (Map.assocs as))
+    ++ "}"
hunk ./TypeInference.hs.old 52
-extendTyEnv :: ValId -> TypeScheme -> TypeEnv -> TypeEnv
-extendTyEnv = Map.insert
hunk ./TypeInference.hs.old 53
-extendTyEnv' :: [(ValId, TypeScheme)] -> TypeEnv -> TypeEnv
-extendTyEnv' assocs env = 
-    foldr (\ (k,v) e -> extendTyEnv k v e) env assocs
+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
hunk ./TypeInference.hs.old 63
-data TIState = TIState { ti_thetaProgram :: InstanceEnv }
+data TIState = TIState { ti_subst :: TypeSubst }
hunk ./TypeInference.hs.old 65
-emptyTIState = TIState { ti_thetaProgram = [] }
+emptyTIState = TIState { ti_subst = nullSubst }
hunk ./TypeInference.hs.old 72
-runTI :: InstanceEnv -> TI a -> ST a
-runTI ie ti = evalStateT ti (emptyTIState { ti_thetaProgram = ie })
+runTI :: TI a -> ST a
+runTI ti = evalStateT ti emptyTIState
hunk ./TypeInference.hs.old 75
-splitConstraints :: [Constraint] -> ([ClassConstraint], [EqConstraint])
-splitConstraints = undefined
+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
hunk ./TypeInference.hs.old 90
---catchTI :: TI a -> [FailureCause] -> (FailureCause -> TI a) -> TI a
---catchTI st causes handler = mkCatchFailure catchST st causes handler
hunk ./TypeInference.hs.old 91
-type TIResult = (([ClassConstraint], [EqConstraint]), TypeSubst, Type)
+type Infer e t = Assumps -> e -> TI ([Constraint], t)
hunk ./TypeInference.hs.old 93
-tiExp :: TypeEnv -> Exp -> TI TIResult
+tiExpr :: Infer Exp Type
+tiExpr as (Var i) = 
+    do let sc = find i as
+       (ps, t) <- freshInst sc
+       return (splitConstraints ps, t)
hunk ./TypeInference.hs.old 99
-tiExp env (Var id) = 
-    let scheme = case lookupTyEnv id env of
-                  Just x -> x
-                  Nothing -> 
-                      phasefail ("variable `" ++ showPpr id ++
-                                 "' not contained in value environment")
-        quants = tyscheme_quants scheme
-        (constrs, ty) = case tyscheme_qtype scheme of
-                          UnconstrainedType t -> ([], t)
-                          ConstrainedType cs t -> (cs, t)
-    in do (constrs', _) <- liftST $ instantiate quants constrs
-          (ty', _) <- liftST $ instantiate quants ty
-          return (splitConstraints constrs', nullSubst, ty')
+tiExpr as (Num _) = return $ (([], []), TyConstruct intTypeId)
hunk ./TypeInference.hs.old 101
-tiExp env (App e1 e2) = 
-    do ((theta1, u1), t1, tau1) <- tiExp env e1
-       ((theta2, u2), t2, tau2) <- tiExp (applySubst t1 env) e2
-       thetaP <- gets ti_thetaProgram
+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
hunk ./TypeInference.hs.old 114
-       -- FIXME: unification missing
-       (u, r) <- (undefined :: TI ([EqConstraint], TypeSubst))
-       let resTheta = applySubst r $ (applySubst t2 theta1) ++ theta2
-           resSubst = r `composeSubst` t2 `composeSubst` t1
-           resType = applySubst r alpha
-       return ((resTheta, u), resSubst, resType)
+       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)
+
+tiExpr as e = 
+    do panic ("tiExpr for " ++ showPpr' e ++ " not yet implemented")
+
+-- 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)
hunk ./TypeInference.hs.old 144
-tiExp env (Lam vars e) = 
-    do (alphas, schemes) <- freshTyVars (length vars)
-       (ctx, t, tau) <- tiExp (extendTyEnv' (zip vars schemes) env) e
-       return (ctx, t, tyApps (applySubst t alphas) tau)
hunk ./TypeInference.hs.old 145
-tiExp env (Let binds exp) = tiExp env (Letrec binds exp)
-       
-tiExp env (Letrec binds exp) =
-    do group <- toBindGroup binds
-       (subst, types) <- tiBindGroup env group
-       (ctx, subst', tau) <- tiExp (applySubst subst (extendTyEnv' types env))
-                                   exp
-       return (ctx, subst' `composeSubst` subst, tau)
+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
hunk ./TypeInference.hs.old 179
-tiImpls :: TypeEnv -> [ImplBind] -> TI (TypeSubst, [(ValId, TypeScheme)])
-tiImpls env binds =
-    do (alphas, schemes) <- freshTyVars (length binds)
-       let ids = map fst binds
-           exps = map snd binds
-           env' = extendTyEnv' (zip ids schemes) env
-       res <- mapM (tiExp env') exps
-       let (ctx, ts, taus) = unzip3 res
-           (thetas, us) = unzip ctx
-       let t = case foldM mergeSubst nullSubst ts of
-                 Left err -> phasefail ("type error: " ++ err)
-                 Right x -> x
-           theta = concat thetas
-           u = concat us
-           sigmas = map (generalize (applySubst t env') theta u) taus
-       return (t, (zip ids sigmas))
+type Expl = (ValId, TypeScheme, Bind)
hunk ./TypeInference.hs.old 181
-tiExpl :: TypeEnv -> [ExplBind] -> TI TypeSubst
-tiExpl = undefined
+-- returns the deferred constraints
+tiExpl :: Assumps -> Expl -> TI ([ClassConstraint], [EqConstraint])
+tiExpl as (i, sc, bind) = 
+    do debug ("typing explicitly type binding " ++ showPpr' i ++ "\n")
+       (ps, t) <- tiBind as bind  -- infered type
+       s <- gets ti_subst
+       let t' = applySubst s t   
+           ps' = mergeConstraints $ 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')
+                `Set.difference` fs
+           sc' = TypeScheme (Set.toList gs) 
+                 (if null ps' then UnconstrainedType t'
+                  else ConstrainedType ps'' t')
+       debug ("type infered for " ++ showPpr' i ++ ": " ++ showPpr sc' ++
+             ", 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 (splitConstraints ds)
hunk ./TypeInference.hs.old 214
-tiBindGroup :: TypeEnv -> BindGroup -> TI (TypeSubst, [(ValId, TypeScheme)])
-tiBindGroup env (BindGroup es iss) =
-    let explTypes = [(id,ty) | (id,ty,exp) <- es] 
-        env' = extendTyEnv' explTypes env
-        in do (subst, implTypes) <- tiIss env' iss
-              let env'' = applySubst subst (extendTyEnv' implTypes env')
-              subst' <- tiExpl env'' es
-              return (subst' `composeSubst` subst, explTypes ++ implTypes)
-    where tiIss _ [] = return (nullSubst, [])
-          tiIss env (i:is) =
-              do (subst, types) <- tiImpls env i
-                 let env' = applySubst subst (extendTyEnv' types env)
-                 (subst', types') <- tiIss env' iss
-                 return (subst' `composeSubst` subst, types ++ types')
hunk ./TypeInference.hs.old 215
-type ExplBind = (ValId, TypeScheme, Exp)
-type ImplBind = (ValId, Exp)
-data BindGroup = BindGroup [ExplBind] [[ImplBind]]
+type Impl = (ValId, Bind)
hunk ./TypeInference.hs.old 217
-toBindGroup :: [ValBind] -> TI BindGroup
--- FIXME
-toBindGroup binds = 
-    do is <- mapM toImpl binds
-       return $ BindGroup [] [is]
-    where toImpl (ValBind _ (Just _) _ _) = 
-              phasefail "explicitly typed bindings not supported atm"
-          toImpl (ValBind id Nothing args exp) =
-              return (id, Lam args exp)
+-- returns the deferred constraints and the types for the bindings
+tiImpls :: Infer [Impl] Assumps
+tiImpls as bs = 
+    do let is = map fst bs
+       debug ("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 (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
+       debug ("monotypes for implicitly type bindings: " ++
+              showCommaListed (map (\ (i, t) -> ppr i <+> text " :: " <+> 
+                                                ppr t) (zip is ts')) ++ 
+              ", constraints: " ++ showCommaListed ps')
+       (ds, rs) <- liftST $ split (Set.toList fs) 
+                              (Set.toList $ foldr1 Set.intersection vss)
+                              ps'
+       (constrs, scs') <-
+           if restricted bs 
+              then
+              let gs' = gs `Set.difference` (freeTypeVars rs)
+                  scs'' = map (\t -> TypeScheme (Set.toList gs')
+                                       (UnconstrainedType t)) ts'
+              in do debug ("The monomorphism restriction applies")
+                    return (ds ++ rs, scs'')
+              else
+              let scs'' = map (\t -> TypeScheme (Set.toList gs) 
+                                       (ConstrainedType rs t)) ts'
+              in do debug ("The monomorphism restriction does not apply")
+                    return (ds, scs'')
+       let resAssumps = buildAssumps is scs'
+       debug ("finished typing implicitly typed bindings, deferred " ++
+              "constraints: " ++ showCommaListed constrs ++ "\n\n" ++
+               (showTypeSigs (Map.assocs resAssumps)) ++ "\n\n")
+       return (splitConstraints constrs, resAssumps)
+    where 
+    restricted :: [Impl] -> Bool
+    restricted bs = 
+        let simple (i, b) = null (fst b)
+            in any simple bs
+    
+{-   
+tiImpls :: Infer [Impl] Assumps
+tiImpls as bs = 
+    let groups = getBindGroups bs fst getDeps
+        in do 
+    where 
+    getDeps (id, (args, e) = [] -- FIXME
hunk ./TypeInference.hs.old 276
--- FIXME: use split in generalization!!
-generalize :: TypeEnv -> [ClassConstraint] -> [EqConstraint] -> Type 
-           -> TypeScheme
-generalize = undefined
+tiImplsSeq :: Infer [[Impl]] Assumps
+tiImplsSeq as [] = return (([], []), emptyAssumps)
+tiImplsSeq as (bs:bss) = 
+    do (ps, as') <- tiImpls as bs
+       (qs, as'') <- tiSeq (as' `merge` as) bss
+       return
+  -}
+tiBindGroup :: Infer [ValBind] Assumps 
+tiBindGroup 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'') <- tiImpls (as' `merge` as) impls
+       debug ("assumptions obtained by typing the implicitly typed bindings: "
+              ++ dumpAssumps as'' ++ ", constraints: " ++ 
+              showCommaListed (mergeConstraints ps))
+       qss <- mapM (tiExpl (as'' `merge` as' `merge` as)) expls
+       let resConstrs = let (q1, q2) = unzipConstraints qss
+                            (p1, p2) = ps
+                            in (q1 ++ p1, q2 ++ p2)
+           resAssumps = as'' `merge` as'
+       mapM checkForAmbiguity (Map.assocs resAssumps)
+       debug ("finished typing binding group " ++ showCommaListed ids ++
+              ", resulting assumptions: " ++ dumpAssumps resAssumps ++ 
+              ", resulting constraints: " 
+              ++ showCommaListed (mergeConstraints resConstrs))
+       return (resConstrs, resAssumps)
+    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)
+    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 ()
hunk ./TypeInference.hs.old 324
+
+tiMain :: Program -> ST Assumps
+tiMain (Program _ _ _ valBinds) = 
+    do debug "\n\n  ==> STARTING TYPE INFERENCE <== \n\n"
+       ((cs,es), as) <- runTI $ ti emptyAssumps valBinds
+       if not (null cs) || not (null es)
+          then panic ("Non-empty set of constraints after type inference:\n" ++
+                      dumpAssumps as ++ "\n" ++ dumpClassConstraints cs ++
+                      "\n" ++ dumpEqConstraints es)
+          else return as
+    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')
+
hunk ./TypeInference.hs.old 362
+
+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
+
+dumpTypeInference :: Assumps -> Program -> String
+dumpTypeInference as (Program _ classes _ binds) =
+    let methods = concatMap dumpMethods classes
+        values = map dumpValue binds
+    in concat (intersperse "\n" $ methods ++ values)
+    where
+    dumpMethods :: ClassDec -> [String]
+    dumpMethods cd = [] -- FIXME map dump (class_tsigs cd)
+    dumpValue :: ValBind -> String
+    dumpValue vb = dump (vbind_name vb)
+    dump i = showTypeSig (i, (find i as))
hunk ./TypeInference.hs.old 406
-freshTyVars n = 
-    do alphas <- liftST $ mapM freshTypeVar 
-                 (take n $ repeat KindStar)
-       return (alphas, map toScheme alphas)
+showTypeSig (i, sc) = showPpr i ++ " :: " ++ showPpr sc
hunk ./TypeInference.hs.old 408
+showTypeSigs l = concat (intersperse "\n" $ map showTypeSig l)
hunk ./Unification.hs 15
+import Maybe (catMaybes, isJust)
+
hunk ./Unification.hs 32
-matchType :: [TypeVarId] -> Type -> Type -> ST TypeSubst
+matchType :: [TypeVarId] -> Type -> Type -> ST (Maybe TypeSubst)
hunk ./Unification.hs 36
-       case mergeSubst sl sr of
-         Nothing -> failwith MatchingFailed 
-                    ("cannot match " ++ showPpr t1 ++ " and " ++ showPpr t2)
-         Just s -> return s
+       case (sl, sr) of
+         (Just sl', Just sr') ->
+             return $ mergeSubst sl' sr'
+         _ -> return Nothing
hunk ./Unification.hs 44
-            then return (u +-> t)
-            else failwith MatchingFailed "kind mismatch"
-matchType _ (TyVar u) (TyVar u') | u == u' = return nullSubst
-matchType _ (TyConstruct id) (TyConstruct id') | id == id' = return nullSubst
+            then return $ Just (u +-> t)
+            else return Nothing
+matchType _ (TyVar u) (TyVar u') | u == u'= return $ Just nullSubst
+matchType _ (TyConstruct id) (TyConstruct id') | id == id' 
+    = return $ Just nullSubst
hunk ./Unification.hs 52
-matchType _ t1 t2 = failwith MatchingFailed ("cannot match " ++ showPpr t1 ++
-                                             " and " ++ showPpr t2)
+matchType _ t1 t2 = return Nothing
hunk ./Unification.hs 54
-matchTypes :: [TypeVarId] -> [Type] -> [Type] -> ST TypeSubst
+matchTypes :: [TypeVarId] -> [Type] -> [Type] -> ST (Maybe TypeSubst)
hunk ./Unification.hs 57
-       case foldM mergeSubst nullSubst substs of
-         Nothing -> failwith MatchingFailed
-                    ("cannot matches types " ++ showPpr t1s ++ " and " ++
-                     showPpr t2s)
-         Just s -> return s
+       if all isJust substs
+          then case foldM mergeSubst nullSubst (catMaybes substs) of
+                 Nothing -> return Nothing
+                 Just s -> return $ Just s
+          else return Nothing
hunk ./Unification.hs 98
-catchUF :: UF a -> [FailureCause] -> (PException -> UF a) -> UF a
-catchUF st causes handler = mkCatchFailure catchST st causes handler
hunk ./Unification.hs 99
-
hunk ./Unification.hs 103
-reductionFailed succ err = catchUF succ [ReductionFailed] (\_ -> err)
+--reductionFailed succ err = catchUF succ [ReductionFailed] (\_ -> err)
hunk ./Unification.hs 105
-reduceOneStep t = 
-    do debug ("reduceOneStep: " ++ showPpr t)
-       res <- reduceOneStep' t
-       debug "reduceOneStep DONE"
-       return res
-
-reduceOneStep' :: Type -> UF Type
+reduceOneStep :: Type -> UF (Maybe Type)
hunk ./Unification.hs 107
-reduceOneStep' (TyApp t1 t2) =
+reduceOneStep (TyApp t1 t2) =
hunk ./Unification.hs 109
-       return $ TyApp t1' t2
-    `reductionFailed`
-    do t2' <- reduceOneStep t2
-       return $ TyApp t1 t2'
+       case t1' of
+         Just x -> return (Just $ TyApp x t2)
+         Nothing ->
+             do t2' <- reduceOneStep t2
+                case t2' of
+                  Just x -> return (Just $ TyApp t1 x)
+                  Nothing -> return Nothing
hunk ./Unification.hs 117
-reduceOneStep' (TyAssoc at@(AssocType id params)) =
+reduceOneStep (TyAssoc at@(AssocType id params)) =
hunk ./Unification.hs 119
-       return $ TyAssoc (AssocType id params')
-    `reductionFailed`
-    do constrs <- gets uf_theta
-       debug "calling reduceAT"
-       res <- liftST $ reduceAT at constrs
-       debug "after reduceAT"
-       return res
+       case params' of
+         Just x -> return (Just $ TyAssoc (AssocType id x))
+         Nothing ->
+             do constrs <- gets uf_theta
+                res <- liftST $ reduceAT at constrs
+                return res
hunk ./Unification.hs 126
-    reduceParam [] = failwith ReductionFailed 
-                     "cannot reduce type synonym application"
+    reduceParam [] = return Nothing
hunk ./Unification.hs 129
-           return (x':xs)
-        `reductionFailed`
-        do xs' <- reduceParam xs
-           return (x:xs')
+           case x' of
+             Just z -> return $ Just (z:xs)
+             Nothing ->
+                 do xs' <- reduceParam xs
+                    case xs' of
+                      Just zs -> return $ Just (x:zs)
+                      Nothing -> return Nothing
hunk ./Unification.hs 139
-    reduceAT :: AssocType -> EqEnv ->  ST Type
-    reduceAT at [] = 
-        failwith ReductionFailed ("cannot reduce type synonym " ++ showPpr' at)
+    reduceAT :: AssocType -> EqEnv ->  ST (Maybe Type)
+    reduceAT at [] = return Nothing
hunk ./Unification.hs 153
-                   -- the result of the reduction is the right-hand side
-                   -- of the (instantiated) equality constraint, after
-                   -- performing the substitution
-                   let res = applySubst subst (eqc_right eq')
-                   debug ("reduction successful, result: " ++ showPpr' res)
-                   E.assert 
-                        (applySubst subst (assoc_params . eqc_left $ eq') 
-                         == params)
-                        (return res)
+                   case subst of
+                     Nothing -> return Nothing
+                     Just s ->
+                     -- the result of the reduction is the right-hand side
+                     -- of the (instantiated) equality constraint, after
+                     -- performing the substitution
+                         let res = applySubst s (eqc_right eq')
+                         in do debug ("reduction successful, result: " 
+                                      ++ showPpr' res)
+                               return $ Just res
hunk ./Unification.hs 164
-reduceOneStep' t = 
-    do debug ("cannot reduce " ++ showPpr t)
-       failwith ReductionFailed ("cannot reduce " ++ showPpr t)
+reduceOneStep t = return Nothing
hunk ./Unification.hs 172
-unifyOneStep eq = 
-    do debug "unifyOneStep"
-       res <- unifyOneStep' eq
-       debug "unifyOneStep DONE"
-       return res
-
-unifyOneStep' :: TypeEq -> UF UFResult'
+unifyOneStep :: TypeEq -> UF (Maybe UFResult')
hunk ./Unification.hs 174
-unifyOneStep' (t1 :=: t2) | t1 == t2 = return (emptyEqs, nullSubst)
+unifyOneStep (t1 :=: t2) | t1 == t2 = return $ Just (emptyEqs, nullSubst)
hunk ./Unification.hs 176
-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 179
-unifyOneStep' (TyApp l r :=: TyApp l' r') = 
-    return ([l :=: l', r :=: r'], nullSubst)
+unifyOneStep (TyApp l r :=: TyApp l' r') = 
+    return $ Just ([l :=: l', r :=: r'], nullSubst)
hunk ./Unification.hs 182
-unifyOneStep' (t1@(TyAssoc _) :=: t2) = oneStepAssoc t1 t2
-unifyOneStep' (t2 :=: t1@(TyAssoc _)) = oneStepAssoc t1 t2
+unifyOneStep (t1@(TyAssoc _) :=: t2) = oneStepAssoc t1 t2
+unifyOneStep (t2 :=: t1@(TyAssoc _)) = oneStepAssoc t1 t2
hunk ./Unification.hs 185
-unifyOneStep' (t1 :=: t2) = 
-    failwith UnificationFailed ("cannot unify `" ++ showPpr t1 ++ "' with `" ++
-                                showPpr t2 ++ "'")
+unifyOneStep (t1 :=: t2) = return Nothing
hunk ./Unification.hs 187
-oneStepVar :: TypeVarId -> Type -> UF UFResult'
-oneStepVar u t | t == TyVar u = return (emptyEqs, nullSubst)
+oneStepVar :: TypeVarId -> Type -> UF (Maybe UFResult')
+oneStepVar u t | t == TyVar u = return $ Just (emptyEqs, nullSubst)
hunk ./Unification.hs 190
-                   failwith UnificationFailed
-                     ("variable `" ++ showPpr u ++ "' occurs in " ++ showPpr t)
+                   do debug "occurs check failed"
+                      return Nothing
hunk ./Unification.hs 196
-                         then return (emptyEqs, u +-> t)
-                         else failwith UnificationFailed
-                               ("kind mismatch while unifying `" ++ 
-                                showPpr u ++ "' with `" ++ showPpr t ++ "'")
+                         then return $ Just (emptyEqs, u +-> t)
+                         else do debug ("kind mismatch while unifying " ++ 
+                                        showPpr' u ++ " with " ++ showPpr' t)
+                                 return Nothing
hunk ./Unification.hs 201
-oneStepAssoc :: Type -> Type -> UF UFResult'
+oneStepAssoc :: Type -> Type -> UF (Maybe UFResult')
hunk ./Unification.hs 204
-       return ([t2 :=: t1], nullSubst)
+       case t2 of
+         Just x -> return $ Just ([x :=: t1], nullSubst)
+         Nothing -> return Nothing
hunk ./Unification.hs 242
+       debug ("after return from unify', remaining equations: " ++
+              showEqs u ++ ", substitution: " ++ showSubst r)
hunk ./Unification.hs 256
-    where adjustConstraint (t :=: TyAssoc at) = 
-              adjustConstraint (TyAssoc at :=: t)
-          adjustConstraint c@(TyAssoc at :=: t) = 
-              case t of
-                TyVar _ -> panic ("Equality constraint `" ++ showPpr c ++ 
-                                  "' in result when unifying " ++ 
-                                  showEqs eqs)
-                _ -> Right $ EqConstraint at t
+    where -- note: even a eq constraint if the form T a = b is acceptable,
+          -- because a might be equal to b.
+          adjustConstraint (TyAssoc at :=: t) = 
+              Right $ EqConstraint at t
+          adjustConstraint (t :=: TyAssoc at) = 
+              Right $ EqConstraint at t
hunk ./Unification.hs 268
-    do debug ("unify' " ++ showEqs eqs)
-       x <- tryOneStep eqs
+    do x <- tryOneStep eqs
hunk ./Unification.hs 270
-         Nothing -> return (eqs, nullSubst)  -- rule refl_U*
+         Nothing -> 
+             do return (eqs, nullSubst)  -- rule refl_U*
hunk ./Unification.hs 277
-oneStepFailed succ err = catchUF succ [ReductionFailed, UnificationFailed] 
-                           (\e -> do debug (show e)
-                                     err)
hunk ./Unification.hs 280
-tryOneStep (eq:rest) = 
-    do debug "tryOneStep"
-       (u',r') <- unifyOneStep eq
-       return $ Just (rest, u', r')
-    `oneStepFailed`
-    do x <- tryOneStep rest
-       case x of
-         Nothing -> return Nothing
-         Just (u, u', r') -> return $ Just (eq:u, u', r')
+tryOneStep l@(eq:rest) = 
+    do res <- unifyOneStep eq
+       case res of
+         Just (u',r') -> return $ Just (rest, u', r')
+         Nothing ->
+             do x <- tryOneStep rest
+                case x of
+                  Nothing -> return Nothing
+                  Just (u, u', r') -> return $ Just (eq:u, u', r')
addfile ./tests/type-inference/should_fail/000.err
hunk ./tests/type-inference/should_fail/000.err 1
+type error while checking explicitly typed binding `foo'
+  infered signature: forall v[-1] . v[-1] -> v[-1]
+  user-supplied signature: forall a b . a -> b
addfile ./tests/type-inference/should_fail/000.mhs
hunk ./tests/type-inference/should_fail/000.mhs 1
+-- the user supplied signature is too general
+foo :: a -> b;
+foo x = x;
addfile ./tests/type-inference/should_fail/001.err
hunk ./tests/type-inference/should_fail/001.err 1
+type error while checking explicitly typed binding `foo'
+  infered signature: forall v[-2] v[-1] . v[-1] -> v[-2] -> v[-1]
+  user-supplied signature: forall a b . a -> b -> b
addfile ./tests/type-inference/should_fail/001.mhs
hunk ./tests/type-inference/should_fail/001.mhs 1
+-- user-supplied signature wrong
+foo :: a -> b -> b;
+foo x y = x;
addfile ./tests/type-inference/should_fail/002.err
hunk ./tests/type-inference/should_fail/002.err 1
+type error while checking explicitly typed binding `foo'
+  infered signature: forall v[-2] v[-1] . v[-1] -> v[-2] -> v[-2]
+  user-supplied signature: forall a[1] . C a[1], T a[1] = Bool => a[1] -> T a[1] -> Int
addfile ./tests/type-inference/should_fail/002.mhs
hunk ./tests/type-inference/should_fail/002.mhs 1
+class C a where {
+  type T a;
+}
+
+foo :: C a, T a = Bool => a -> T a -> Int;
+foo x y = y;
addfile ./tests/type-inference/should_fail/003.err
hunk ./tests/type-inference/should_fail/003.err 1
+type error while checking explicitly typed binding `bar'
+  infered signature: forall v[-3] . C v[-3], T v[-3] = Bool => v[-3] -> Int
+  user-supplied signature: forall a[2] . C a[2] => a[2] -> Int
addfile ./tests/type-inference/should_fail/003.mhs
hunk ./tests/type-inference/should_fail/003.mhs 1
+class C a where {
+  type T a;
+}
+
+foo :: C a, T a = Bool => a -> Int;
+foo x = 42;
+
+bar :: C a => a -> Int;
+bar y = foo y;
+
addfile ./tests/type-inference/should_fail/004.err
hunk ./tests/type-inference/should_fail/004.err 1
+type error while checking explicitly typed binding `foobar'
+  infered signature: forall v[-1] . v[-1] -> Int
+  user-supplied signature: forall a[1] . C a[1] => a[1] -> T a[1]
addfile ./tests/type-inference/should_fail/004.mhs
hunk ./tests/type-inference/should_fail/004.mhs 1
+class C a where {
+  type T a;
+}
+
+foobar :: C a => a -> T a;
+foobar x = 412;
+
+
addfile ./tests/type-inference/should_fail/005.err
hunk ./tests/type-inference/should_fail/005.err 1
+Cannot unify {Int -> v[-4] -> T v[-4] = Bool -> v[-8]}. Unsatisfiable equality constraint: Int = Bool
addfile ./tests/type-inference/should_fail/005.mhs
hunk ./tests/type-inference/should_fail/005.mhs 1
+data T a = D Int a;
+
+foo x = D True x;
+
addfile ./tests/type-inference/should_fail/006.err
hunk ./tests/type-inference/should_fail/006.err 1
+Cannot unify {Int = Bool}. Unsatisfiable equality constraint: Int = Bool
addfile ./tests/type-inference/should_fail/006.mhs
hunk ./tests/type-inference/should_fail/006.mhs 1
+foo = if 1 then True else False;
addfile ./tests/type-inference/should_fail/007.err
hunk ./tests/type-inference/should_fail/007.err 1
+Cannot unify {Bool = Int}. Unsatisfiable equality constraint: Bool = Int
addfile ./tests/type-inference/should_fail/007.mhs
hunk ./tests/type-inference/should_fail/007.mhs 1
+foo = if True then 1 else False;
addfile ./tests/type-inference/should_fail/008.mhs
hunk ./tests/type-inference/should_fail/008.mhs 1
+class C c where {
+  type T c;
+}
+
+undefined = undefined;
+
+foo :: C a => a -> T a;
+foo = undefined;
+
+bar :: C a => a -> Int;
+bar x = foo x + 4;
addfile ./tests/type-inference/should_fail/Flag
hunk ./tests/type-inference/should_fail/Flag 1
+expect-fail --no-location
addfile ./tests/type-inference/should_fail/ambiguous1.err
hunk ./tests/type-inference/should_fail/ambiguous1.err 1
+ambiguous signature for `foo': forall a[1] . C a[1] => T a[1] -> T a[1]
addfile ./tests/type-inference/should_fail/ambiguous1.mhs
hunk ./tests/type-inference/should_fail/ambiguous1.mhs 1
+class C a where {
+  type T a;
+}
+
+foo :: C a => T a -> T a;
+foo x = x;
+
addfile ./tests/type-inference/should_pass/000.mhs
hunk ./tests/type-inference/should_pass/000.mhs 1
+foo :: a -> a;
+foo x = x;
addfile ./tests/type-inference/should_pass/000.out
hunk ./tests/type-inference/should_pass/000.out 1
+foo :: forall a . a -> a
addfile ./tests/type-inference/should_pass/001.mhs
hunk ./tests/type-inference/should_pass/001.mhs 1
+foo :: b -> b -> b;
+foo x y = x;
addfile ./tests/type-inference/should_pass/001.out
hunk ./tests/type-inference/should_pass/001.out 1
+foo :: forall b . b -> b -> b
addfile ./tests/type-inference/should_pass/002.mhs
hunk ./tests/type-inference/should_pass/002.mhs 1
+foo :: b -> Int -> b;
+foo x y = x;
addfile ./tests/type-inference/should_pass/002.out
hunk ./tests/type-inference/should_pass/002.out 1
+foo :: forall b . b -> Int -> b
addfile ./tests/type-inference/should_pass/003.mhs
hunk ./tests/type-inference/should_pass/003.mhs 1
+class C c where {
+  type T c;
+}
+
+foo :: C a => a -> T a -> Int;
+foo x y = 42;
addfile ./tests/type-inference/should_pass/003.out
hunk ./tests/type-inference/should_pass/003.out 1
+foo :: forall a . C a => a -> T a -> Int
addfile ./tests/type-inference/should_pass/004.mhs
hunk ./tests/type-inference/should_pass/004.mhs 1
+class C c where {
+  type T c;
+}
+
+foo :: C a, T a = Bool => a -> T a -> Bool;
+foo x y = y;
addfile ./tests/type-inference/should_pass/004.out
hunk ./tests/type-inference/should_pass/004.out 1
+foo :: forall a . C a, T a = Bool => a -> T a -> Bool
addfile ./tests/type-inference/should_pass/005.mhs
hunk ./tests/type-inference/should_pass/005.mhs 1
+class C c where {
+  type T c;
+}
+
+foo :: C a, T a = Bool => a -> Int;
+foo x = 42;
+
+bar :: C b, T b = Bool => b -> Int;
+bar y = foo y;
+
addfile ./tests/type-inference/should_pass/005.out
hunk ./tests/type-inference/should_pass/005.out 1
+foo :: forall a . C a, T a = Bool => a -> Int
+bar :: forall b . C b, T b = Bool => b -> Int
addfile ./tests/type-inference/should_pass/006.mhs
hunk ./tests/type-inference/should_pass/006.mhs 1
+-- test for deferring a constraint to the enclosing scope
+class C a where {
+}
+
+foo :: C a => a -> Int;
+foo x = 42;
+
+bar :: C a => a -> Int;
+bar x = letrec f :: Int -> Int;
+               f y = y + foo x;
+        in f 1;
addfile ./tests/type-inference/should_pass/006.out
hunk ./tests/type-inference/should_pass/006.out 1
+foo :: forall a[1] . C a[1] => a[1] -> Int
+bar :: forall a[2] . C a[2] => a[2] -> Int
addfile ./tests/type-inference/should_pass/007.mhs
hunk ./tests/type-inference/should_pass/007.mhs 1
+foo x = bar x;
+bar y = foo y;
addfile ./tests/type-inference/should_pass/007.out
hunk ./tests/type-inference/should_pass/007.out 1
+foo :: forall v[-4] v[-3] . v[-3] -> v[-4]
+bar :: forall v[-4] v[-3] . v[-3] -> v[-4]
addfile ./tests/type-inference/should_pass/008.mhs
hunk ./tests/type-inference/should_pass/008.mhs 1
+class C a where {
+}
+
+foo :: C a => a -> Int;
+foo x = 42;
+
+bar x = letrec f y = y + foo x;
+        in f 1;
addfile ./tests/type-inference/should_pass/008.out
hunk ./tests/type-inference/should_pass/008.out 1
+foo :: forall a[1] . C a[1] => a[1] -> Int
+bar :: forall v[-2] . C v[-2] => v[-2] -> Int
addfile ./tests/type-inference/should_pass/009.mhs
hunk ./tests/type-inference/should_pass/009.mhs 1
+class C a where {
+}
+
+foo :: C a => a -> Int;
+foo x = 42;
+
+-- the monomorphism restriction does not apply
+bar x y = letrec f z = foo z;
+          in f x + f y;
addfile ./tests/type-inference/should_pass/009.out
hunk ./tests/type-inference/should_pass/009.out 1
+foo :: forall a[1] . C a[1] => a[1] -> Int
+bar :: forall v[-3] v[-2] . C v[-3], C v[-2] => v[-2] -> v[-3] -> Int
addfile ./tests/type-inference/should_pass/010.mhs
hunk ./tests/type-inference/should_pass/010.mhs 1
+-- Test for monomorphism restriction
+class C a where {
+}
+
+foo :: C a => a -> Int;
+foo x = 42;
+
+-- x and y must have the same type because of monomorphism restriction applied to f
+bar x y = letrec f = \z -> foo z;
+          in f x + f y;
addfile ./tests/type-inference/should_pass/010.out
hunk ./tests/type-inference/should_pass/010.out 1
+foo :: forall a[1] . C a[1] => a[1] -> Int
+bar :: forall v[-3] . C v[-3] => v[-3] -> v[-3] -> Int
addfile ./tests/type-inference/should_pass/011.mhs
hunk ./tests/type-inference/should_pass/011.mhs 1
+class C c where {
+  type T c;
+}
+
+foo :: C a => a -> T a -> T a;
+foo x y = y;
+
+bar x = foo x;
addfile ./tests/type-inference/should_pass/011.out
hunk ./tests/type-inference/should_pass/011.out 1
+foo :: forall a . C a => a -> T a -> T a
+bar :: forall v[-2] . C v[-2] => v[-2] -> T v[-2] -> T v[-2]
addfile ./tests/type-inference/should_pass/012.mhs
hunk ./tests/type-inference/should_pass/012.mhs 1
+class C c where {
+  type T c;
+}
+
+foo :: C a => a -> T a -> T a;
+foo x y = y;
+
+bar x = foo x x;
addfile ./tests/type-inference/should_pass/012.out
hunk ./tests/type-inference/should_pass/012.out 1
+foo :: forall a . C a => a -> T a -> T a
+bar :: forall v[-2] . T v[-2] = v[-2], C v[-2] => v[-2] -> T v[-2]
addfile ./tests/type-inference/should_pass/013.mhs
hunk ./tests/type-inference/should_pass/013.mhs 1
+-- Test for ensuring the binding groups are splitted correctly
+id x = x;
+f = id g;
+g = 1 + f;
addfile ./tests/type-inference/should_pass/013.out
hunk ./tests/type-inference/should_pass/013.out 1
+id :: forall v[-2] . v[-2] -> v[-2]
+f :: Int
+g :: Int
addfile ./tests/type-inference/should_pass/014.mhs
hunk ./tests/type-inference/should_pass/014.mhs 1
+data T a = D1 a Int
+         | D2 Bool
+;
+
+foo = D1 True 42;
addfile ./tests/type-inference/should_pass/015.mhs
hunk ./tests/type-inference/should_pass/015.mhs 1
+x = (42, False);
addfile ./tests/type-inference/should_pass/016.mhs
hunk ./tests/type-inference/should_pass/016.mhs 1
-
+x :: (Int, Bool);
+x = (42, True);
addfile ./tests/type-inference/should_pass/017.mhs
hunk ./tests/type-inference/should_pass/017.mhs 1
+data T a = D1 a Int
+         | D2 Bool
+;
+
+foo x = (D1 x 42, D2 True);
addfile ./tests/type-inference/should_pass/018.mhs
hunk ./tests/type-inference/should_pass/018.mhs 1
-
+foo x y = 1 + (if x then 42 else y);
addfile ./tests/type-inference/should_pass/019.mhs
hunk ./tests/type-inference/should_pass/019.mhs 1
+class C c where {
+  type T c;
+}
+
+undefined = undefined;
+
+foo :: C a => a -> T a;
+foo = undefined;
+
+bar x = foo x + 4;
addfile ./tests/type-inference/should_pass/020.mhs
hunk ./tests/type-inference/should_pass/020.mhs 1
+class C c where {
+  type T c;
+}
+
+undefined = undefined;
+
+bar :: C a => a -> T a;
+bar x = undefined;
+
+foo z = letrec f y = bar z;
+               g y = 1 + f y;
+        in g 42
+;
addfile ./tests/type-inference/should_pass/Flag
hunk ./tests/type-inference/should_pass/Flag 1
+--dump-infer
}