[complete tyinfer for expressions, added support for methods
mail@stefanwehr.de**20050523092913] {
hunk ./Error.hs 27
-    debug_, enableDebug,
+    debug_, info_, enableDebug, DebugLevel(..),
hunk ./Error.hs 34
+import Char (toUpper)
hunk ./Error.hs 40
+import System.IO                      ( hFlush, stdout )
hunk ./Error.hs 102
+
+data DebugLevel = Debug
+                | Info 
+                | Disabled
+                  deriving (Eq,Ord,Show)
+
+genDebug :: MonadIO m => DebugLevel -> Location -> String -> m ()
+genDebug level (fname, lineno) msg = 
+    let s = "[" ++ map toUpper (show level) ++ "] " ++ fname  ++ ":" 
+            ++ show lineno ++ ": " ++ msg
+        in do l <- liftIO $ readIORef debugFlag
+              if level >= l 
+                 then liftIO $ do (putStrLn s) 
+                                  hFlush stdout 
+                 else return ()
hunk ./Error.hs 119
-debug_ (fname, lineno) msg = 
-    let s = "[DEBUG] " ++ fname  ++ ":" ++ show lineno ++ ": " ++ msg
-        in do f <- liftIO $ readIORef debugFlag
-              if f then liftIO (putStrLn s) else return ()
+debug_ loc msg = genDebug Debug loc msg
+
+info_ :: MonadIO m => Location -> String -> m ()
+info_ loc msg = genDebug Info loc msg
+
+enableDebug :: DebugLevel -> IO ()
+enableDebug l =
+    writeIORef debugFlag l
+
+debugFlag :: IORef DebugLevel
+debugFlag = unsafePerformIO (newIORef Disabled)
+{-# NOINLINE debugFlag #-}
hunk ./Error.hs 139
-enableDebug :: IO ()
-enableDebug =
-    writeIORef debugFlag True
hunk ./Error.hs 140
-debugFlag :: IORef Bool
-debugFlag = unsafePerformIO (newIORef False)
-{-# NOINLINE debugFlag #-}
hunk ./IdMap.hs 7
-data IdMap a b c d e f g = IdMap { typeVarMap :: Map.Map TypeVarId a,
-                                   typeMap :: Map.Map TypeId b,
-                                   valMap :: Map.Map ValId c,
-                                   dataMap :: Map.Map DataId d,
-                                   classMap :: Map.Map ClassId e,
-                                   assocTypeMap :: Map.Map AssocTypeId f,
-                                   methodMap :: Map.Map MethodId g }
+data IdMap a b c d e f = IdMap { typeVarMap :: Map.Map TypeVarId a,
+                                 typeMap :: Map.Map TypeId b,
+                                 valMap :: Map.Map ValId c,
+                                 dataMap :: Map.Map DataId d,
+                                 classMap :: Map.Map ClassId e,
+                                 assocTypeMap :: Map.Map AssocTypeId f }
hunk ./IdMap.hs 15
-emptyIdMap = IdMap e e e e e e e 
+emptyIdMap = IdMap e e e e e e
hunk ./IdMap.hs 20
-     Map.elems (dataMap m), Map.elems (classMap m), Map.elems (assocTypeMap m),
-     Map.elems (methodMap m))
+     Map.elems (dataMap m), Map.elems (classMap m), Map.elems (assocTypeMap m))
hunk ./IdMap.hs 23
-             (f -> f'), (g -> g'))
-         -> IdMap a b c d e f g
-         -> IdMap a' b' c' d' e' f' g'
-mapIdMap (a, b, c, d, e, f, g) m = 
+             (f -> f'))
+         -> IdMap a b c d e f
+         -> IdMap a' b' c' d' e' f'
+mapIdMap (a, b, c, d, e, f) m = 
hunk ./IdMap.hs 32
-            assocTypeMap = Map.map f (assocTypeMap m),
-            methodMap = Map.map g (methodMap m) }
+            assocTypeMap = Map.map f (assocTypeMap m) }
hunk ./IdMap.hs 43
-insertMethod k v m = m { methodMap = Map.insert k v (methodMap m) }
hunk ./IdMap.hs 55
-lookupMethod k m = saveLookup k (methodMap m)
hunk ./KindInference.hs 52
-type KindEnv = IdMap Kind' Kind' Kind' Kind' Kind' Kind' Kind'
+type KindEnv = IdMap Kind' Kind' Kind' Kind' Kind' Kind'
hunk ./KindInference.hs 156
-       let (a,b,c,d,e,f,g) = elemsIdMap env
-           allKinds = a ++ b ++ c ++ d ++ e ++ f ++ g
+       let (a,b,c,d,e,f) = elemsIdMap env
+           allKinds = a ++ b ++ c ++ d ++ e ++ f
hunk ./KindInference.hs 191
-        in modifyEnv $ mapIdMap (a, a, a, a, a, a, a)
+        in modifyEnv $ mapIdMap (a, a, a, a, a, a)
hunk ./KindInference.hs 416
-
hunk ./KindInference.hs 417
-kiQualifiedType (ConstrainedType cs ty) =
+kiQualifiedType (QualifiedType cs ty) =
hunk ./KindInference.hs 420
-kiQualifiedType (UnconstrainedType ty) = kiType ty
hunk ./Main.hs 49
+import List (find)
hunk ./Main.hs 64
+        dump p = dump' flags p
hunk ./Main.hs 67
-            do WFP.check ast
+            do info "\n  ==> WELL-FORMEDNESS 1 <==\n"
+               WFP.check ast
+                  
+               info "\n  ==> KIND INFERENCE <==\n"
hunk ./Main.hs 72
+
+               info "\n  ==> WELL-FORMEDNESS 2 <==\n"
hunk ./Main.hs 76
-                    do liftIO $ dump (ppr ast)
-                       kiDump <- dumpKindInference ast
-                       liftIO $ dump kiDump
+                    do kiDump <- dumpKindInference ast
+                       liftIO $ dump $ (ppr ast) $$ kiDump
+                              
+               info "\n   ==> TYPE INFERENCE <==\n"
hunk ./Main.hs 85
-dump :: Pretty p => p -> IO ()
-dump p = do hPutStrLn stdout (showPpr p)
-            return ()
+dump' :: Pretty p => [Flag] -> p -> IO ()
+dump' fs p =
+    let s = showPpr p
+        in if not (null s)
+              then do hPutStrLn stdout (showPpr p)
+                      if ExitAfterDump `elem` fs
+                         then exitWith ExitSuccess
+                         else return ()
+              else return ()
hunk ./Main.hs 104
+    let dump p = dump' flags p
hunk ./Main.hs 106
-    when (on Debug) enableDebug
+    case debugLevel flags of
+      Nothing -> return ()
+      Just l -> enableDebug l
hunk ./Main.hs 124
+      info "\n  ==> LEXING <==\n"
hunk ./Main.hs 129
+      info "\n  ==> PARSING <==\n"
hunk ./Main.hs 135
-      ast <- evaluate (transform parseSyntax)
+      info "\n  ==> SYNTAX TRANSFORMATION <==\n"
+      ast <- (transform parseSyntax)
hunk ./Main.hs 168
+debugLevel :: [Flag] -> Maybe DebugLevel
+debugLevel [] = Nothing
+debugLevel (DebugLevel l:_) = Just l
+debugLevel (_:rest) = debugLevel rest
+
hunk ./Main.hs 175
-    | Debug
+    | DebugLevel DebugLevel
hunk ./Main.hs 178
+    | ExitAfterDump
hunk ./Main.hs 208
-    , Option []    ["debug"] (NoArg Debug) "enable debug messages"
+    , Option []    ["debug"] (NoArg (DebugLevel Debug)) "enable debug messages"
+    , Option []    ["info"] (NoArg (DebugLevel Info)) "enable info messages"
+    , Option []    ["exit-after-dump"] (NoArg ExitAfterDump) 
+            "terminate the program after dumping"
hunk ./ParseSyntax.hs 32
-type MethodId = UniqIdents.MethodId
hunk ./ParseSyntax.hs 45
-type MethodId = Id
hunk ./ParseSyntax.hs 73
-type VSig = (MethodId, TypeScheme)
+type VSig = (ValId, TypeScheme)
hunk ./ParseSyntax.hs 79
-                             inst_valBinds :: [MethodBind]
+                             inst_valBinds :: [ValBind]
hunk ./ParseSyntax.hs 90
-data MethodBind = MethodBind { method_name :: MethodId, 
-                               method_params :: [ValId],
-                               method_exp :: Exp
-                             }
-  deriving (Read,Show,Eq, Gen.Data, Gen.Typeable)
hunk ./ParseSyntax.hs 198
-data QualifiedType 
-    = ConstrainedType [Constraint] Type
-    | UnconstrainedType Type
+
+data QualifiedType = QualifiedType { qtype_context :: [Constraint],
+                                     qtype_mono    :: Type }
hunk ./ParseSyntax.hs 203
-splitQType :: QualifiedType -> ([Constraint], Type)
-splitQType (ConstrainedType cs t) = (cs, t)
-splitQType (UnconstrainedType t) = ([], t)
-
hunk ./ParseSyntax.hs 204
-    = TypeScheme { tyscheme_quants :: [TypeVarId],
-                   tyscheme_qtype :: QualifiedType
+    = TypeScheme { tyscheme_quants   :: [TypeVarId],
+                   tyscheme_qtype    :: QualifiedType
hunk ./ParseSyntax.hs 255
-    applySubst s (ConstrainedType c t) = 
-        ConstrainedType (applySubst s c) (applySubst s t)
-    applySubst s (UnconstrainedType t) = 
-        UnconstrainedType (applySubst s t)
+    applySubst s (QualifiedType c t) = 
+        QualifiedType (applySubst s c) (applySubst s t)
hunk ./ParseSyntax.hs 259
-    freeTypeVars (ConstrainedType c t) = 
+    freeTypeVars (QualifiedType c t) = 
hunk ./ParseSyntax.hs 261
-    freeTypeVars (UnconstrainedType t) = freeTypeVars t
-    fixedTypeVars (UnconstrainedType t) = fixedTypeVars t
-    fixedTypeVars (ConstrainedType c t) = 
+    fixedTypeVars (QualifiedType c t) = 
hunk ./ParseSyntax.hs 264
+
hunk ./ParseSyntax.hs 266
-    applySubst s (TypeScheme quant t) =
+    applySubst s (TypeScheme quant qt) =
hunk ./ParseSyntax.hs 268
-            in TypeScheme quant (applySubst s' t)
+            in TypeScheme quant (applySubst s' qt)
hunk ./ParseSyntax.hs 331
-    | Let    [ValBind] Exp  -- let x = e1 in e2
hunk ./ParseSyntax.hs 343
-data Alt = Alt DataId [ValId] Exp   -- tag var -> exp
+data Alt = Alt { alt_name :: DataId,
+                 alt_params ::[ValId],
+                 alt_exp :: Exp
+               }
hunk ./ParseSyntax.hs 381
+
hunk ./ParseSyntax.hs 384
-    pprPrec prec (ConstrainedType constrs ty) = 
+    pprPrec prec (QualifiedType constrs ty) = 
hunk ./ParseSyntax.hs 391
-    pprPrec prec (UnconstrainedType ty) = pprPrec prec ty
hunk ./ParseSyntax.hs 475
-instance Pretty MethodBind where
-    ppr (MethodBind x vars e) = 
-        ppr x <+> hsep (map ppr vars) <=> ppr e
-
hunk ./ParseSyntax.hs 518
-    pprPrec prec (Let bs e) = 
-        parens `usedWhen` (prec > minPrec) $ 
-        text "let" $$ nest 4 
-                           (vcat $ intersperse semi (map ppr bs)) $$
-                               hang (text "in") 4 (ppr e)
-
hunk ./ParseSyntax.hs 520
-        text "letrec" $$ nest 4 
+        text "let" $$ nest 4 
hunk ./Parser.y 175
-methodBinds :: { [MethodBind] }
+methodBinds :: { [ValBind] }
hunk ./Parser.y 179
-methodBind :: { MethodBind }
-    : var vars '=' exp              { MethodBind $1 $2 $4 }
+methodBind :: { ValBind }
+    : var vars '=' exp              { ValBind $1 Nothing $2 $4 }
hunk ./Parser.y 212
-    | 'let' valBinds 'in' exp           { Let (reverse $2) $4     }
-    | 'letrec' valBinds 'in' exp        { Letrec (reverse $2) $4     }
+    | 'let' valBinds 'in' exp           { Letrec (reverse $2) $4     }
hunk ./Parser.y 267
-	: context '=>' type		{ ConstrainedType  $1 $3 }
-	| type				{ UnconstrainedType $1 }
+	: context '=>' type		{ QualifiedType  $1 $3 }
+	| type				{ QualifiedType [] $1 }
hunk ./ParserHelper.hs 17
-            TypeDef "->" ["a", "b"] [],
+            TypeDef "->" ["@a", "@b"] [],
hunk ./ParserHelper.hs 19
-            TypeDef "(,)" ["a", "b"] [DataConstructor "Pair"
-                                      [TyVar "a", TyVar "b"]]]
+            TypeDef "(,)" ["@a", "@b"] [DataConstructor "Pair"
+                                       [TyVar "@a", TyVar "@b"]]]
hunk ./ParserHelper.hs 43
-mkClassInst :: ([Constraint], Type) -> AssocTypeBind -> [MethodBind] 
+mkClassInst :: ([Constraint], Type) -> AssocTypeBind -> [ValBind] 
hunk ./Symtab.hs 14
+  findMethodSig,
hunk ./Symtab.hs 81
+findMethodSig :: ClassId -> ValId -> ST VSig
+findMethodSig cid i =
+    do cdec <- findClass cid
+       case List.find ((==) i . fst) (class_vsigs cdec) of
+         Just vsig -> return vsig
+         Nothing -> phasefail ("Method " ++ showPpr' i ++ " is not defined in "
+                               ++ "class " ++ showPpr cid)
+
hunk ./Symtab.hs 137
-               [TypeVarId] -> c -> ST (c, [TypeVarId])
+               [TypeVarId] -> c -> ST (c, [TypeVarId], Subst TypeVarId Type)
hunk ./Symtab.hs 142
-       return (applySubst subst c, freshs)
+       return (applySubst subst c, freshs, subst)
hunk ./Symtab.hs 236
+-- * inserts the class
+-- * inserts the signatures of the associated types
hunk ./Symtab.hs 246
+-- * registers the instances as a instance of its class
+-- * enters the associated type definitions in the equality environment
hunk ./SyntaxTransformation.hs 32
-                          AssocTypeId, MethodId, ValId)
+                          AssocTypeId, ValId)
hunk ./SyntaxTransformation.hs 44
-transform :: Program -> AS.Program
+transform :: Program -> IO AS.Program
hunk ./SyntaxTransformation.hs 57
+     info "rewriting type definitions ..."
hunk ./SyntaxTransformation.hs 59
+     info "rewriting class declarations ..."
hunk ./SyntaxTransformation.hs 61
+     info "rewriting instance declarations ..."
hunk ./SyntaxTransformation.hs 63
+     info "rewriting bindings ..."
hunk ./SyntaxTransformation.hs 103
-       vsigs' <- mapM rw_vsig vsigs
+       vsigs' <- mapM (rw_vsig name param) vsigs
hunk ./SyntaxTransformation.hs 117
-rw_vsig:: VSig -> NA AS.VSig
-rw_vsig (i, t) = 
-  do uid <- defineMethod i
-     t' <- rw_typeScheme t
-     return (uid, t')
-
+rw_vsig:: ClassId -> TypeVarId -> VSig -> NA AS.VSig
+rw_vsig cid tv (i, sc) = 
+  do uid <- defineValVar i
+     sc' <- rw_typeScheme sc
+     return (uid, sc')
hunk ./SyntaxTransformation.hs 143
-rw_classBinds:: [MethodBind] -> NA [AS.MethodBind]
+rw_classBinds:: [ValBind] -> NA [AS.ValBind]
hunk ./SyntaxTransformation.hs 145
-    where rw_classBind :: MethodBind -> NA AS.MethodBind
-          rw_classBind (MethodBind id params exp) =
-              do uid <- lookUpMethod id
+    where rw_classBind :: ValBind -> NA AS.ValBind
+          rw_classBind (ValBind id (Just _) params exp) =
+              panic ("explicitly typed method binding should not be produced "
+                     ++ "by the parser")
+          rw_classBind (ValBind id Nothing params exp) =
+              do uid <- lookUpValVar id
hunk ./SyntaxTransformation.hs 155
-                 return (AS.MethodBind uid params' exp')
+                 return (AS.ValBind uid Nothing params' exp')
hunk ./SyntaxTransformation.hs 183
-rw_typeScheme (TypeScheme [] qtype) = 
+rw_typeScheme (TypeScheme [] qtype@(QualifiedType _ t)) = 
hunk ./SyntaxTransformation.hs 185
-       let free = case qtype of
-                    UnconstrainedType _ -> undef
-                    ConstrainedType _ t -> 
-                        undef `List.intersect` freeTypeVarsList t
+       let free = undef `List.intersect` freeTypeVarsList t
hunk ./SyntaxTransformation.hs 195
-rw_qualifiedType (ConstrainedType constrs t) = 
+rw_qualifiedType (QualifiedType constrs t) = 
hunk ./SyntaxTransformation.hs 198
-       return (AS.ConstrainedType constrs' t')
-
-rw_qualifiedType (UnconstrainedType t) = 
-    do t' <- rw_type t
-       return (AS.UnconstrainedType t')
+       return (AS.QualifiedType constrs' t')
hunk ./SyntaxTransformation.hs 315
-rwExp (Let binds e)    = 
-   do triples <- mapM rw_bind binds
-      enterBlock
-      names <- mapM defineBind binds
-      e' <- rwExp e
-      exitBlock
-      let binds' = map mkBind (zip names triples)
-      return (AS.Let binds' e')
- 
hunk ./TypeInference.hs 7
-import List (partition, intersperse)
+import List (partition, intersperse, filter,nub)
hunk ./TypeInference.hs 31
-                                "' not found in assumptions")
+                                "' not found in assumptions: " ++
+                                dumpAssumps as)
hunk ./TypeInference.hs 114
-    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)
+    do sc <- liftST $ typeOfDataConstructor di
+       (ps, t) <- freshInst sc
hunk ./TypeInference.hs 119
-           ty' =  tyFuns operandTypes alpha
-       qs <- unify [] ty ty'
-       return (map EC qs ++ concat pss, alpha)
+           t' =  tyFuns operandTypes alpha
+       qs <- unify [] t t'
+       return (ps ++ map EC qs ++ concat pss, alpha)
hunk ./TypeInference.hs 154
-tiExpr as e = 
-    do panic ("tiExpr for " ++ showPpr' e ++ " not yet implemented")
+tiExpr as (Case e alts) = 
+    do (ps, t) <- tiExpr as e
+       l <- mapM (\ (Alt di params _) -> tiPat di params) alts
+       let (pss, ts, ass) = unzip3 l
+       qss <- mapM (unify [] t) ts
+       let es = map alt_exp alts
+       l' <- mapM (\ (as', e') -> tiExpr (as' `merge` as) e') (zip ass es)
+       let (rss, resTys) = unzip l'
+       alpha <- liftST $ freshTypeVar KindStar
+       qss' <- mapM (unify [] alpha) resTys
+       return (concat (pss ++ rss) ++ map EC (concat (qss ++ qss')), 
+               alpha)
+    where
+    tiPat :: DataId -> [ValId] -> TI ([Constraint], Type, Assumps)
+    tiPat di paramIds = 
+        do ts <- liftST $ mapM (\_ -> freshTypeVar KindStar) paramIds
+           t' <- liftST $ freshTypeVar KindStar
+           sc <- liftST $ typeOfDataConstructor di
+           (qs, t) <- freshInst sc
+           ps <- unify [] t (tyFuns ts t')
+           return (map EC ps ++ qs, t', buildAssumps paramIds (map toScheme ts))
+    
hunk ./TypeInference.hs 191
-subsumes sc1@(TypeScheme quants1 qt1) sc2@(TypeScheme quants2 qt2) = 
+subsumes sc1@(TypeScheme quants1 (QualifiedType pi1 tau1))
+         sc2@(TypeScheme quants2 qt2) = 
hunk ./TypeInference.hs 198
-           qt2' = applySubst subst qt2
-           (pi2', tau2') = splitQType qt2'
+           QualifiedType pi2' tau2' = applySubst subst qt2
hunk ./TypeInference.hs 202
-           (pi1, tau1) = splitQType qt1
hunk ./TypeInference.hs 228
-    do debug ("typing explicitly type binding " ++ showPpr' i ++ "\n")
+    do info ("typing explicitly typed binding " ++ showPpr' i)
+       debug (dumpAssumps as)
hunk ./TypeInference.hs 242
-           sc' = TypeScheme (Set.toList gs) 
-                 (if null ps' then UnconstrainedType t'
-                  else ConstrainedType ps'' t')
+           sc' = TypeScheme (Set.toList gs) (QualifiedType ps'' t')
hunk ./TypeInference.hs 264
-       debug ("typing implicitly typed bindings " ++ showCommaListed is)
+       info ("typing implicitly typed bindings " ++ showCommaListed is)
+       debug (dumpAssumps as)
hunk ./TypeInference.hs 272
-           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 ()
+       pss' <- mapM (uncurry $ unify []) (zip ts types)
+       let ps = concat pss ++ (map EC $ concat pss')
hunk ./TypeInference.hs 284
+       debug (dumpAssumps (applySubst s as))
hunk ./TypeInference.hs 293
-                                       (UnconstrainedType t)) ts'
+                                       (QualifiedType [] t)) ts'
hunk ./TypeInference.hs 298
-                                       (ConstrainedType rs t)) ts'
+                                       (QualifiedType rs t)) ts'
hunk ./TypeInference.hs 368
+                  ||
+                  -- 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))
hunk ./TypeInference.hs 378
-              
hunk ./TypeInference.hs 380
-tiMain (Program _ _ _ valBinds) = 
-    do debug "\n\n  ==> STARTING TYPE INFERENCE <== \n\n"
-       (ps, as) <- runTI $ ti emptyAssumps valBinds
+tiMain (Program _ classes instances valBinds) = 
+    do (ps, as) <- runTI $ ti classes instances valBinds
hunk ./TypeInference.hs 386
-    where ti as binds = 
-              do (ctx, as') <- tiBindGroup as binds
+    where ti classes instances binds = 
+              do -- insert the methods into the assumptions
+                 let methodsSigs = concatMap rwMethodSigs classes
+                     (names, schemes) = unzip methodsSigs
+                     as = buildAssumps names schemes
+                 -- type the "regular" bindings
+                 (ps, as') <- tiBindGroup as binds
+                 let as'' = as' `merge` as
+                 -- check the types of the methods
+                 info ("checking types of method implementations")
+                 mapM (checkMethods as'') instances
hunk ./TypeInference.hs 398
-                 return (applySubst s ctx, applySubst s as')
+                 return (applySubst s ps, applySubst s as'')
+          -- for a method declaration in class `D a', we must add the
+          -- `D a' to the constraints and `a' to the quantified variables
+          -- of its signature.
+          rwMethodSigs :: ClassDec -> [VSig]
+          rwMethodSigs cdec = 
+              let selfConstraint = CC $ ClassConstraint (class_name cdec)
+                                        (TyVar (class_param cdec))
+                  rw (TypeScheme qs (QualifiedType cs t)) = 
+                     TypeScheme (nub (class_param cdec : qs))
+                                (QualifiedType
+                                    (nub (selfConstraint : cs)) t)
+                  in map (\ (i,sc) -> (i, rw sc)) (class_vsigs cdec)
+          checkMethods :: Assumps -> ClassInst -> TI ()
+          checkMethods as ci = 
+              mapM_ (checkMethod as ci) (inst_valBinds ci)
+          checkMethod :: Assumps -> ClassInst -> ValBind -> TI ()
+          checkMethod as ci (ValBind i _ params e) =
+              do let cid = inst_class ci
+                 -- we must construct the expected type of the implementation
+                 (_, TypeScheme qs (QualifiedType cs t)) <- 
+                     liftST (findMethodSig cid i)
+                 cdec <- liftST $ findClass cid
+                 let cs' = List.nub (inst_constraints ci ++ cs)
+                     t' = applySubst (class_param cdec +-> inst_type ci) t
+                     qs' = List.nub (qs ++ freeTypeVarsList (inst_type ci))
+                     sc' = TypeScheme qs' (QualifiedType cs' t')
+                 debug ("checking definition of method " ++ showPpr' i ++ 
+                        " of class " ++ showPpr cid ++ " in instance for "
+                        ++ showPpr' (inst_type ci) ++ ". Expected type: " ++
+                        showPpr' sc')
+                 ps <- tiExpl as (i, sc', (params, e))
+                 if not (null ps)
+                    then panic ("Non-empty set of constraints after checking "++
+                                "the type of a method: " ++
+                                dumpAssumps as ++ "\n" ++ dumpConstraints ps)
+                    else return ()
hunk ./TypeInference.hs 451
-       (constrs, ty) = case tyscheme_qtype sc of
-                         UnconstrainedType t -> ([], t)
-                         ConstrainedType cs t -> (cs, t)
-   in do ((constrs', ty'), _) <- liftST $ instantiate quants (constrs, ty)
+       QualifiedType constrs ty = tyscheme_qtype sc 
+   in do ((constrs', ty'), _, _) <- liftST $ instantiate quants (constrs, ty)
hunk ./TypeInference.hs 456
-toScheme t = TypeScheme [] (UnconstrainedType t)
+toScheme t = TypeScheme [] (QualifiedType [] t)
+
+typeOfDataConstructor :: DataId -> ST TypeScheme
+typeOfDataConstructor di = 
+    do (tydef, dataCons) <- findDataConstructor di
+       let quants = tydef_params tydef
+           tc = TyConstruct (tydef_name tydef)
+           resTy = foldl TyApp tc (map TyVar quants)
+           t = tyFuns (dconstr_params dataCons) resTy
+       return $ TypeScheme quants (QualifiedType [] t)
+                               
hunk ./TypeInference.hs 501
-    let methods = concatMap dumpMethods classes
-        values = map dumpValue binds
-    in concat (intersperse "\n" $ methods ++ values)
+    let values = map dumpValue binds
+    in concat (intersperse "\n" $ values)
hunk ./TypeInference.hs 504
-    dumpMethods :: ClassDec -> [String]
-    dumpMethods cd = [] -- FIXME map dump (class_tsigs cd)
hunk ./Unification.hs 147
-                   (eq', freshs) <- instantiate quants eq
+                   (eq', freshs, _) <- instantiate quants eq
hunk ./UniqIdents.hs 6
-  TypeVarId, TypeId, DataId, ClassId, AssocTypeId, MethodId, ValId,
+  TypeVarId, TypeId, DataId, ClassId, AssocTypeId, ValId,
hunk ./UniqIdents.hs 19
-  defineAssocTypeCon, defineClass, defineMethod,
+  defineAssocTypeCon, defineClass, 
hunk ./UniqIdents.hs 22
-  lookUpAssocTypeCon, lookUpClass, lookUpMethod,
+  lookUpAssocTypeCon, lookUpClass, 
hunk ./UniqIdents.hs 30
+
+import qualified Data.Generics as Gen
+import Control.Monad.State
hunk ./UniqIdents.hs 36
-import qualified Data.Generics as Gen
hunk ./UniqIdents.hs 64
-    deriving (Eq,Show,Read,Ord,Gen.Typeable,Gen.Data)
-newtype MethodId = MethodId Id 
hunk ./UniqIdents.hs 82
-
-instance Pretty MethodId where
-    ppr (MethodId id) = ppr id
hunk ./UniqIdents.hs 123
-                       | Method MethodId 
hunk ./UniqIdents.hs 129
-newtype NA r = NA (NAState -> (r, NAState))
-unNA:: NA r -> NAState -> (r, NAState)
-unNA (NA m) = m
+type NA = StateT NAState IO
hunk ./UniqIdents.hs 131
-instance Monad NA where
-  return r = NA $ \s -> (r, s)
-  m >>= n  = NA $ \s -> let (r, s') = unNA m s in unNA (n r) s'
-  fail s   = panic ("fail in the NA monad: " ++ s)
hunk ./UniqIdents.hs 134
-runNA :: NA a -> a
-runNA m = 
-  let (r, s) = unNA m emptyNAState in r
+runNA :: NA a -> IO a
+runNA m = evalStateT m emptyNAState
hunk ./UniqIdents.hs 137
-get :: (NAState -> a) -> NA a
-get f = NA $ \s -> (f s, s)
-
-setValueLevel x = NA $ \s -> ((), s { na_valueLevel = x })
-setTypeVars x = NA $ \s -> ((), s { na_typeVars = x })
-setTypeLevel x = NA $ \s -> ((), s { na_typeLevel = x })
-setVersions x = NA $ \s -> ((), s { na_versions = x })
+setValueLevel x = modify (\s -> s { na_valueLevel = x })
+setTypeVars x = modify (\s -> s { na_typeVars = x })
+setTypeLevel x = modify (\s -> s { na_typeLevel = x })
+setVersions x = modify (\s -> s { na_versions = x })
hunk ./UniqIdents.hs 147
-    do m <- get na_versions
+    do m <- gets na_versions
hunk ./UniqIdents.hs 163
-       m <- get a
+       m <- gets a
hunk ./UniqIdents.hs 183
-
-defineMethod :: ParseId -> NA MethodId
-defineMethod = defineValue MethodId Method NS.defGlobal "method"
hunk ./UniqIdents.hs 204
-    do m <- get a
+    do m <- gets a
hunk ./UniqIdents.hs 218
-lookUpMethod :: ParseId -> NA MethodId
-lookUpMethod = lookUpValue NS.findGlobal 
-                 (\w -> case w of 
-                          Method uid -> Just uid
-                          _ -> Nothing) "method variable"
hunk ./UniqIdents.hs 248
-    do m <- get na_typeLevel
+    do m <- gets na_typeLevel
hunk ./UniqIdents.hs 255
-    do m <- get na_typeVars
+    do m <- gets na_typeVars
hunk ./UniqIdents.hs 264
-    do m <- get na_typeVars
+    do m <- gets na_typeVars
hunk ./UniqIdents.hs 271
-    do ns <- get na_valueLevel
+    do ns <- gets na_valueLevel
hunk ./UniqIdents.hs 276
-    do ns <- get na_valueLevel
+    do ns <- gets na_valueLevel
hunk ./WellFormedProgram.hs 38
-    do mapM checkOverlappingInstances classDecs
+    do debug "checking overlapping instances"
+       mapM checkOverlappingInstances classDecs
hunk ./WellFormedProgram.hs 74
-    do mapM checkClassDec classDecs
+    do info "checking class declarations"
+       mapM checkClassDec classDecs
+       info "checking instance declarations"
hunk ./WellFormedProgram.hs 78
+       info "checking bindings"
hunk ./WellFormedProgram.hs 80
+       info "checking associated type applications"
hunk ./WellFormedProgram.hs 132
-    checkClassParamUnconstrained (mid, TypeScheme _ (ConstrainedType c _)) = 
-        if param `Set.member` freeTypeVars c
+    checkClassParamUnconstrained (mid, TypeScheme _ (QualifiedType cs _)) = 
+        if param `Set.member` freeTypeVars cs
hunk ./WellFormedProgram.hs 138
-    checkClassParamUnconstrained _ = return ()
-    checkFixv (mid, ts) = 
-        if not $ param `Set.member` fixedTypeVars ts
+    checkFixv (mid, sc) = 
+        if not $ param `Set.member` fixedTypeVars sc
hunk ./WellFormedProgram.hs 144
-    checkEqConstraints (_, TypeScheme _ (ConstrainedType cs _)) = 
+    checkEqConstraints (_, TypeScheme _ (QualifiedType cs _)) = 
hunk ./WellFormedProgram.hs 147
-    checkEqConstraints (_, _) = return ()
hunk ./WellFormedProgram.hs 236
-    cmpVbind b1 b2 = method_name b1 `compare` method_name b2
-    checkMethodDefinition ((id,_), mb) | id == method_name mb = return ()
+    cmpVbind b1 b2 = vbind_name b1 `compare` vbind_name b2
+    checkMethodDefinition ((id,_), mb) | id == vbind_name mb = return ()
hunk ./WellFormedProgram.hs 361
-checkBind b@(ValBind _ (Just (TypeScheme _ (ConstrainedType cs _))) _ e) = 
-    do mapM checkConstraint cs
+checkBind b@(ValBind i (Just (TypeScheme _ (QualifiedType cs _))) _ e) = 
+    do debug ("checking binding " ++ showPpr' i)
+       mapM checkConstraint cs
hunk ./pp/macros.m4 8
+define(info, (info_ `SRC_LOC_'))dnl
hunk ./tests/ast/should_fail/007.mhs 1
-main = letrec x = 4;
-              x = 3;
+main = let x = 4;
+           x = 3;
addfile ./tests/ast/should_fail/010.err
hunk ./tests/ast/should_fail/010.err 1
+illegal instance declaration for class C: methods do not match
addfile ./tests/ast/should_fail/010.mhs
hunk ./tests/ast/should_fail/010.mhs 1
+class C a where {
+  type T a;
+  foo :: a -> Int;
+}
+
+bar = 10;
+
+instance C Int where {
+  type T Int = Bool;
+  foo i = i;
+  bar = 21;
+}
hunk ./tests/ast/should_pass/000.out 5
-data -> 1 2 =
+data -> @a @b =
hunk ./tests/ast/should_pass/000.out 8
-data (,) 3 4 =
-    Pair 3 4
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
hunk ./tests/ast/should_pass/001.out 5
-data -> 1 2 =
+data -> @a @b =
hunk ./tests/ast/should_pass/001.out 8
-data (,) 3 4 =
-    Pair 3 4
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
hunk ./tests/ast/should_pass/002.out 5
-data -> 1 2 =
+data -> @a @b =
hunk ./tests/ast/should_pass/002.out 8
-data (,) 3 4 =
-    Pair 3 4
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
hunk ./tests/ast/should_pass/003.out 5
-data -> 1 2 =
+data -> @a @b =
hunk ./tests/ast/should_pass/003.out 8
-data (,) 3 4 =
-    Pair 3 4
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
hunk ./tests/ast/should_pass/004.out 5
-data -> 1 2 =
+data -> @a @b =
hunk ./tests/ast/should_pass/004.out 8
-data (,) 3 4 =
-    Pair 3 4
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
hunk ./tests/ast/should_pass/005.out 5
-data -> 1 2 =
+data -> @a @b =
hunk ./tests/ast/should_pass/005.out 8
-data (,) 3 4 =
-    Pair 3 4
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
hunk ./tests/ast/should_pass/006.mhs 23
-       in letrec bar = foo + 1;
+       in let bar = foo + 1;
hunk ./tests/ast/should_pass/006.out 5
-data -> 1 2 =
+data -> @a @b =
hunk ./tests/ast/should_pass/006.out 8
-data (,) 3 4 =
-    Pair 3 4
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
hunk ./tests/ast/should_pass/007.out 5
-data -> 1 2 =
+data -> @a @b =
hunk ./tests/ast/should_pass/007.out 8
-data (,) 3 4 =
-    Pair 3 4
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
hunk ./tests/ast/should_pass/Flag 1
---dump-ast
+--dump-ast --exit-after-dump
addfile ./tests/kind-inference/should_fail/000.err
hunk ./tests/kind-inference/should_fail/000.err 1
+attempt to unify these two kinds: Kfun Star (KVar 1), Star
hunk ./tests/kind-inference/should_fail/000.mhs 2
+
addfile ./tests/kind-inference/should_fail/001.err
hunk ./tests/kind-inference/should_fail/001.err 1
+attempt to unify these two kinds: Star, Kfun Star Star
hunk ./tests/kind-inference/should_fail/001.mhs 5
+
addfile ./tests/kind-inference/should_fail/002.err
hunk ./tests/kind-inference/should_fail/002.err 1
+attempt to unify these two kinds: Star, Kfun Star Star
hunk ./tests/kind-inference/should_pass/000.mhs 2
+
addfile ./tests/kind-inference/should_pass/000.out
hunk ./tests/kind-inference/should_pass/000.out 1
+data Int =
+data Bool =
+    False
+    | True
+data -> @a @b =
+data Unit =
+    ()
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
+data T a b =
+    D (a b)
+@a :: *
+@b :: *
+a :: * -> *
+b :: *
+@a[1] :: *
+@b[1] :: *
+Int :: *
+Bool :: *
+-> :: * -> * -> *
+Unit :: *
+(,) :: * -> * -> *
+T :: (* -> *) -> * -> *
hunk ./tests/kind-inference/should_pass/001.mhs 10
+
addfile ./tests/kind-inference/should_pass/001.out
hunk ./tests/kind-inference/should_pass/001.out 1
+data Int =
+data Bool =
+    False
+    | True
+data -> @a @b =
+data Unit =
+    ()
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
+data S a =
+    S1 (a Int)
+    | S2 Unit
+    | S3 (D a)
+data D b =
+    D1 (S b)
+class () => C c where
+    bar :: c Int -> (D c, Bool)
+@a :: *
+@b :: *
+a :: * -> *
+b :: * -> *
+c :: * -> *
+@a[1] :: *
+@b[1] :: *
+Int :: *
+Bool :: *
+-> :: * -> * -> *
+Unit :: *
+(,) :: * -> * -> *
+S :: (* -> *) -> *
+D :: (* -> *) -> *
hunk ./tests/kind-inference/should_pass/002.mhs 1
-data D a b = D (a b) b;
-
-class C1 c where {
-  type T c;
-  foo :: c Int -> d -> Bool -> D c Int;
-}
-
-class C1 e => C2 e where {
-}
-
-instance C1 (D Int) where {
-  type T (D Int) = Bool;
-  foo = 42;
-}
rmfile ./tests/kind-inference/should_pass/002.mhs
hunk ./tests/kind-inference/should_pass/Flag 1
---no-location --dump-kindinfer
+--exit-after-dump --no-location --dump-kindinfer
addfile ./tests/kind-inference/should_pass/depGroups.out
hunk ./tests/kind-inference/should_pass/depGroups.out 1
+data Int =
+data Bool =
+    False
+    | True
+data -> @a @b =
+data Unit =
+    ()
+data (,) @a[1] @b[1] =
+    Pair @a[1] @b[1]
+data D1 =
+    D1[1]
+data D2 =
+    D2[1] D1
+data D3 =
+    D3[1] D4
+data D4 =
+    D4[1] D3 D1
+class () => C1 a where
+    foo :: a -> D3
+class (C1 a[1]) => C2 a[1] where
+@a :: *
+@b :: *
+a :: *
+@a[1] :: *
+@b[1] :: *
+a[1] :: *
+Int :: *
+Bool :: *
+-> :: * -> * -> *
+Unit :: *
+(,) :: * -> * -> *
+D1 :: *
+D2 :: *
+D3 :: *
+D4 :: *
hunk ./tests/tyinfer/should_fail/ambiguous2.mhs 1
-class C a where {
-  type T a;
-}
-
-foo :: C a => T a -> T a;
-foo x = x;
-
rmfile ./tests/tyinfer/should_fail/ambiguous2.mhs
hunk ./tests/tyinfer/should_fail/ambiguous3.mhs 1
-class C a where {
-  type T a;
-}
-
-class D b where {
-    foo :: C a => b -> T a -> T a;
-}
rmfile ./tests/tyinfer/should_fail/ambiguous3.mhs
rmdir ./tests/tyinfer/should_fail
hunk ./tests/tyinfer/should_pass/000.mhs 1
-
-equal x y = True;
-
-bar x = equal  x x;
-
-
rmfile ./tests/tyinfer/should_pass/000.mhs
hunk ./tests/tyinfer/should_pass/001.mhs 1
-data List a =  Cons a (List a) | Nil;
-
-
-class Num a where {
-  sumNumList:: List a -> a;
-}
-
-class Eq a where {
-  equal  :: a -> a -> Bool;
-  dummy  :: a -> a -> a;
-}
-class Collects c where {
-  type Elem c;
-  empty :: c;
-  insert:: Elem c -> c -> c;
-  toList:: c -> List c;
-}
-
-instance Eq e => Collects (e -> Bool) where {
-  type Elem (e -> Bool) = e;
-  empty = let f x = False ;
-          in f;
-  insert e es = Cons e es;}
-
-instance Eq Int where {
-  type Elem (e -> Bool) = e;
-  equal x y = True;
-  dummy x y = x;
-}
-
-mkList x = Cons x Nil;
-
-f1 = mkList;
-
-f2 xs = sumNumList (sumNumList xs);
-
-tst = equal 1 1;
-
-
-
-sumColl ys = sumNumList (toList ys);
-
-bar x = equal x x;
-
--- insertTwo :: (Collects c => (Elem c -> Elem c -> c -> c));
-insertTwo k l coll = insert l (insert k coll);
-
-
--- foo:: a -> a;
-foo x = 
-  let y = 3;
-  in x;
-
-
-main = 1 + 2 + (foo 3);
rmfile ./tests/tyinfer/should_pass/001.mhs
hunk ./tests/tyinfer/should_pass/002.mhs 1
-class Collects c where {
-  type Elem c;
-  empty :: c;
-  insert:: Elem c -> c -> c;
-  -- toList:: c -> List c;
-}
-class Eq a where {
-  equal  :: a -> a -> Bool;
-  dummy  :: a -> a -> a;
-}
-
-instance Eq e => Collects (e -> Bool) where {
-  type Elem (e -> Bool) = e;
-  empty = let f x = False ;
-          in f;
-  insert e es = Cons e es;}
-
-instance Eq Int where {
-  type Elem (e -> Bool) = e;
-  equal x y = True;
-  dummy x y = x;
-}
-
--- insertTwo :: (Collects c => (Elem c -> Elem c -> c -> c));
-insertTwo k l coll = insert l (insert k coll);
-
-
rmfile ./tests/tyinfer/should_pass/002.mhs
hunk ./tests/tyinfer/should_pass/003.mhs 1
-class Num a where {
-  sumNumList:: List a -> a;
-}
-
-class Collects c where {
-  type Elem c;
-  empty :: c;
-  insert:: Elem c -> c -> c;
-  toList:: c -> List (Elem c);
-}
-
-
-
-
-sumColl ys = sumNumList (toList ys);
-
-merge c1 c2 = foldr insert c2 (toList c1)
rmfile ./tests/tyinfer/should_pass/003.mhs
hunk ./tests/tyinfer/should_pass/004.mhs 1
-class Nat n where {
-  type Add n m;
-  f:: Int -> Int;
-}
-
-instance Nat Zero where {
-  type Add Zero m = m;
-  f x = 1;
-}
-
-instance Nat n => Nat (Succ n) where {
-  type Add (Succ n) m = Succ (Add n m);
-  f x = 1;
-}
- 
-
-
-
-
-
-h x  y = y;
-main = 1;
-
-
rmfile ./tests/tyinfer/should_pass/004.mhs
hunk ./tests/tyinfer/should_pass/005.mhs 1
-class Nat n where {
-  type Add n m;
-  f:: Int -> Int;
-}
-class Nat n => VecBound n where {
-  type Vec n a;
- appVec :: (VecBound m =>  (VecBound (Add n m) => (Vec n a -> Vec m a -> Vec (Add n m) a)));
-}
-
-
-
-instance VecBound Zero where {
-  type Vec Zero a = VecZero;
-  appVec xs ys = ys;
-}
-
-
-instance VecBound n => VecBound (Succ n) where {
-  type Vec (Succ n) a = VecSucc;
-  appVec x xs  ys = Cons x (appVec xs ys);
---  appVec (Cons x xs) ys = Cons x (appVec xs ys);
-}
-
-
--- data VecZero = Nil 
--- data VecBound n => VecSucc a = Cons a (Vec n a)
-
-main x = 1;
rmfile ./tests/tyinfer/should_pass/005.mhs
hunk ./tests/tyinfer/should_pass/006.mhs 1
-class Nat n where {
-  type Add n m;
-}
-
-class NNat n where {
-  type AAdd n m;
-}
-
-h x  y = y;
-main = 1;
-
-
rmfile ./tests/tyinfer/should_pass/006.mhs
hunk ./tests/tyinfer/should_pass/007.mhs 1
-class Eq a where {
-  equal  :: a -> a -> Bool;
-  dummy  :: a -> a -> a;
-}
-
-
-main x = equal x x;
rmfile ./tests/tyinfer/should_pass/007.mhs
hunk ./tests/tyinfer/should_pass/008.mhs 1
-data Simp = A | B;
-data List a =  Cons a (List a) | Nil;
-
-foo x = Cons (Cons A Nil) Nil;
-
-main x = A;
rmfile ./tests/tyinfer/should_pass/008.mhs
hunk ./tests/tyinfer/should_pass/009.mhs 1
-foo x = 
-  letrec
-     g = (x,x);
-  in 1;
-
-main x = 1;
rmfile ./tests/tyinfer/should_pass/009.mhs
hunk ./tests/tyinfer/should_pass/collects.mhs 1
-class Eq a where {
-  equal  :: a -> a -> Bool;
-  dummy  :: a -> a -> a;
-}
-
-class Collects c where {
-  type Elem c;
-  empty :: c;
-  insert:: Elem c -> c -> c;
-  -- toList:: c -> List c;
-}
-
-
-instance Eq e => Collects (e -> Bool) where {
-  type Elem (e -> Bool) = e;
-  empty = let f x = False ;
-          in f;
-  insert e es = Cons e es;}
-
-instance Eq Int where {
-  type Elem (e -> Bool) = e;
-  equal x y = True;
-  dummy x y = x;
-}
-
-
-insertTwo x y coll = insert y (insert x coll);
-
-
-foo x = 
-  let y = 3;
-  in x;
-
-main = 1 + 2 + (foo 3);
rmfile ./tests/tyinfer/should_pass/collects.mhs
rmdir ./tests/tyinfer/should_pass
rmdir ./tests/tyinfer
addfile ./tests/type-inference/should_fail/008.err
hunk ./tests/type-inference/should_fail/008.err 1
+type error while checking explicitly typed binding `bar'
+  infered signature: forall v[-4] . T v[-4] = Int, C v[-4] => v[-4] -> Int
+  user-supplied signature: forall a[1] . C a[1] => a[1] -> Int
addfile ./tests/type-inference/should_fail/009.err
hunk ./tests/type-inference/should_fail/009.err 1
+Cannot unify {Bool = T}. Unsatisfiable equality constraint: Bool = T
addfile ./tests/type-inference/should_fail/009.mhs
hunk ./tests/type-inference/should_fail/009.mhs 1
+data T = D Bool;
+
+foo = case True of
+        True -> 1;
+        D x -> 2;
+;
addfile ./tests/type-inference/should_fail/010.err
hunk ./tests/type-inference/should_fail/010.err 1
+Cannot unify {Bool = Int}. Unsatisfiable equality constraint: Bool = Int
addfile ./tests/type-inference/should_fail/010.mhs
hunk ./tests/type-inference/should_fail/010.mhs 1
+foo = case True of
+        True -> 1;
+        False -> False;
+;
addfile ./tests/type-inference/should_fail/011.err
hunk ./tests/type-inference/should_fail/011.err 1
+type error while checking explicitly typed binding `foo'
+  infered signature: forall v[-3] . v[-3] -> v[-3]
+  user-supplied signature: Int -> Bool
addfile ./tests/type-inference/should_fail/011.mhs
hunk ./tests/type-inference/should_fail/011.mhs 1
+class C a where {
+  type T a;
+  foo :: a -> Bool;
+}
+
+instance C Int where {
+  type T Int = Bool;
+  foo = id;
+}
+
+id x = x;
addfile ./tests/type-inference/should_fail/012.err
hunk ./tests/type-inference/should_fail/012.err 1
+context reduction failed for C Int
addfile ./tests/type-inference/should_fail/012.mhs
hunk ./tests/type-inference/should_fail/012.mhs 1
+class C a where {
+  type T a;
+  foo :: a -> Int;
+}
+
+f = foo 1;
addfile ./tests/type-inference/should_fail/013.err
hunk ./tests/type-inference/should_fail/013.err 1
+context reduction failed for C Int
addfile ./tests/type-inference/should_fail/013.mhs
hunk ./tests/type-inference/should_fail/013.mhs 1
+data D a = D a;
+
+class C a where {
+  type T a;
+  foo :: a -> Int;
+}
+
+instance C a => C (D a) where {
+  type T (D a) = Int;
+  foo x = case x of
+            D y -> foo y;
+  ;
+}
+
+bar = foo (D 42);
addfile ./tests/type-inference/should_fail/ambiguous2.err
hunk ./tests/type-inference/should_fail/ambiguous2.err 1
+ambiguous signature for `foo': forall v[-3] . T v[-4] = v[-4], C v[-4] => v[-3] -> Int
addfile ./tests/type-inference/should_fail/ambiguous2.mhs
hunk ./tests/type-inference/should_fail/ambiguous2.mhs 1
+class C c where {
+  type T c;
+}
+
+undefined = undefined;
+
+bar :: C a => a -> T a;
+bar x = undefined;
+
+foo z = let f = bar f;
+        in 42;
hunk ./tests/type-inference/should_pass/006.mhs 9
-bar x = letrec f :: Int -> Int;
-               f y = y + foo x;
+bar x = let f :: Int -> Int;
+            f y = y + foo x;
hunk ./tests/type-inference/should_pass/008.mhs 7
-bar x = letrec f y = y + foo x;
+bar x = let f y = y + foo x;
hunk ./tests/type-inference/should_pass/009.mhs 8
-bar x y = letrec f z = foo z;
+bar x y = let f z = foo z;
hunk ./tests/type-inference/should_pass/010.mhs 9
-bar x y = letrec f = \z -> foo z;
+bar x y = let f = \z -> foo z;
addfile ./tests/type-inference/should_pass/014.out
hunk ./tests/type-inference/should_pass/014.out 1
+foo :: T Bool
addfile ./tests/type-inference/should_pass/015.out
hunk ./tests/type-inference/should_pass/015.out 1
+x :: (Int, Bool)
hunk ./tests/type-inference/should_pass/016.mhs 1
-x :: (Int, Bool);
-x = (42, True);
+x :: (Int -> a) -> (a, Bool);
+x y = (y 42, True);
+
+
addfile ./tests/type-inference/should_pass/016.out
hunk ./tests/type-inference/should_pass/016.out 1
+x :: forall a . (Int -> a) -> (a, Bool)
addfile ./tests/type-inference/should_pass/017.out
hunk ./tests/type-inference/should_pass/017.out 1
+foo :: forall v[-13] v[-2] . v[-2] -> (T v[-2], T v[-13])
hunk ./tests/type-inference/should_pass/018.mhs 1
-foo x y = 1 + (if x then 42 else y);
+class C c where {
+}
+
+bar :: C a => a -> Int;
+bar a = 42;
+
+foo x y z = 1 + (if x then bar y else bar z);
addfile ./tests/type-inference/should_pass/018.out
hunk ./tests/type-inference/should_pass/018.out 1
+bar :: forall a[1] . C a[1] => a[1] -> Int
+foo :: forall v[-4] v[-3] . C v[-4], C v[-3] => Bool -> v[-3] -> v[-4] -> Int
addfile ./tests/type-inference/should_pass/019.out
hunk ./tests/type-inference/should_pass/019.out 1
+undefined :: forall v[-1] . v[-1]
+foo :: forall a . C a => a -> T a
+bar :: forall v[-3] . T v[-3] = Int, C v[-3] => v[-3] -> Int
hunk ./tests/type-inference/should_pass/020.mhs 10
-foo z = letrec f y = bar z;
-               g y = 1 + f y;
-        in g 42
-;
+foo z = let f x = bar (f x);
+        in 42;
addfile ./tests/type-inference/should_pass/020.out
hunk ./tests/type-inference/should_pass/020.out 1
+undefined :: forall v[-1] . v[-1]
+bar :: forall a . C a => a -> T a
+foo :: forall v[-3] . v[-3] -> Int
addfile ./tests/type-inference/should_pass/021.mhs
hunk ./tests/type-inference/should_pass/021.mhs 1
-
+data T x = D x;
+
+data S x y = S1 (x Int) y
+           | S2 y
+           | S3
+;
+
+foo j = case S2 j of
+          S1 a b -> case a of D i -> i;;
+          S2 c -> c;
+          S3 -> 0;
+;
addfile ./tests/type-inference/should_pass/021.out
hunk ./tests/type-inference/should_pass/021.out 1
+foo :: Int -> Int
addfile ./tests/type-inference/should_pass/022.mhs
hunk ./tests/type-inference/should_pass/022.mhs 1
-
+class C a where {
+  type T a;
+  foo :: a -> Int;
+}
+
+instance C Int where {
+  type T Int = Int;
+  foo = id;
+}
+
+instance C Bool where {
+  type T Bool = Bool;
+  foo b = if b then 1 else 0;
+}
+
+id x = x;
+
+bar = (foo 42, foo False);
addfile ./tests/type-inference/should_pass/022.out
hunk ./tests/type-inference/should_pass/022.out 1
+id :: forall v[-2] . v[-2] -> v[-2]
+bar :: (Int, Int)
addfile ./tests/type-inference/should_pass/023.mhs
hunk ./tests/type-inference/should_pass/023.mhs 1
-
+data D a = D a;
+
+class C a where {
+  type T a;
+  foo :: a -> Int;
+}
+
+instance C (D a) where {
+  type T (D a) = Int;
+  foo x = 42;
+}
+
+bar = (foo (D False), foo (D 42));
addfile ./tests/type-inference/should_pass/023.out
hunk ./tests/type-inference/should_pass/023.out 1
+bar :: (Int, Int)
addfile ./tests/type-inference/should_pass/024.mhs
hunk ./tests/type-inference/should_pass/024.mhs 1
+data D a = D a;
+
+class C a where {
+  type T a;
+  foo :: a -> Int;
+}
+
+instance C a => C (D a) where {
+  type T (D a) = Int;
+  foo x = case x of
+            D y -> foo y;
+  ;
+}
+
+instance C Int where {
+  type T Int = Int;
+  foo i = i;
+}
+
+bar = foo (D 42);
addfile ./tests/type-inference/should_pass/024.out
hunk ./tests/type-inference/should_pass/024.out 1
+bar :: Int
addfile ./tests/type-inference/should_pass/025.mhs
hunk ./tests/type-inference/should_pass/025.mhs 1
+class C a where {
+  type T a;
+  foo :: a -> Int;
+}
+
+instance C Int where {
+  type T Int = Int;
+  foo i = i;
+}
+
+instance C Bool where {
+  type T Bool = Bool;
+  foo b = 42;
+}
+
+f = foo 1;
+g = foo True;
addfile ./tests/type-inference/should_pass/025.out
hunk ./tests/type-inference/should_pass/025.out 1
+f :: Int
+g :: Int
hunk ./tests/well-formed/should_fail/eq_constraint3.mhs 5
-bar x = letrec foo :: T Int a = Bool => a -> b -> Bool;
-               foo x y = True;
+bar x = let foo :: T Int a = Bool => a -> b -> Bool;
+            foo x y = True;
addfile ./tests/well-formed/should_fail/overlapping2.err
hunk ./tests/well-formed/should_fail/overlapping2.err 1
+overlapping instances for class C2
}