[added support for methods and for several AT per instance
mail@stefanwehr.de**20050524084828] {
move ./WellFormedProgram.hs ./WellFormedness.hs
hunk ./Entailment.hs 23
-    = do eqEnv <- getEqEnv 
-         ures <- runUnifyAssertEmpty eqEnv [t :=: t'] 
-         case ures of
-           Right s -> return $ Just s
-           Left err -> return Nothing
+    = do debug ("matchConstraint `" ++ showPpr id ++ " " ++ showPpr t ++ "', `"
+                ++ showPpr id' ++ " " ++ showPpr t' ++ "'")
+         eqEnv <- getEqEnv
+         -- first normalize the type
+         tn <- runUF eqEnv (normalise t)
+         tn' <- runUF eqEnv (normalise t')
+         -- then use match to see if there is a substitution s such that
+         -- applySubst s t = t'
+         matchType tn tn'
hunk ./Entailment.hs 44
--- then the list of subgols.
+-- then the list of subgoals.
hunk ./Entailment.hs 57
--- entail uses the program's class and equality constraints implicitly
+-- entail uses the program's class and equality constraints implicitly,
+-- i.e. `entail cs c' checks if `Theta, cs ||- c' holds, where Theta are
+-- the program constraints.
+-- FIXME: The constraints in cs and the constraint c are not quantified.
+-- Atm, I simply do not quantify over any variable. Don't know if this is ok.
hunk ./Entailment.hs 64
-    do debug ("checking if " ++ dumpConstraints cs ++ " entails " ++
+    do debug ("checking if " ++ dumpConstraints cs ++ " entail " ++
hunk ./Entailment.hs 68
-          then debug (dumpConstraints cs ++ " entails " ++ showPpr' c)
-          else debug (dumpConstraints cs ++ " does not entail " ++ showPpr' c)
+          then debug (dumpConstraints cs ++ " entail " ++ showPpr' c)
+          else debug (dumpConstraints cs ++ " do not entail " ++ showPpr' c)
hunk ./Entailment.hs 82
-    do -- FIXME: don't know how to quantify the equality scheme.
-       -- For now, I do not quantify over any variables
-       let ps' = mapMaybe toEqScheme ps
+    do let ps' = mapMaybe toEqScheme ps
hunk ./KindInference.hs 387
-       kiAssocTypeBind (inst_typeBind ci)
+       mapM kiAssocTypeBind (inst_typeBinds ci)
hunk ./Main.hs 33
-import qualified WellFormedProgram as WFP
+import qualified WellFormedness as WF
hunk ./Main.hs 68
-               WFP.check ast
+               WF.check ast
hunk ./Main.hs 74
-               WFP.checkAfterKindInference ast
+               WF.checkAfterKindInference ast
hunk ./ParseSyntax.hs 78
-                             inst_typeBind :: AssocTypeBind,
+                             inst_typeBinds :: [AssocTypeBind],
hunk ./ParseSyntax.hs 276
+instance Substitution TypeVarId Type EqScheme where
+    applySubst s (EqScheme quant c) = 
+        let s' = removeListFromSubst quant s
+            in EqScheme quant (applySubst s' c)
+
+instance Types EqScheme where
+    freeTypeVars (EqScheme quant c) = 
+        freeTypeVars c `Set.difference` (Set.fromList quant)
+    fixedTypeVars (EqScheme quant c) = 
+        fixedTypeVars c `Set.difference` (Set.fromList quant)
+    
hunk ./Parser.y 139
-  : 'instance' head 'where' '{' assocType ';' methodBinds '}' 
-    { mkClassInst $2 $5 (reverse $7)}
+  : 'instance' head 'where' '{' assocTypeBinds methodBinds '}' 
+    { mkClassInst $2 (reverse $5) (reverse $6)}
hunk ./Parser.y 142
-assocType:: { AssocTypeBind }
+assocTypeBinds :: { [AssocTypeBind] }
+    : assocTypeBinds assocTypeBind ';'  { $2 : $1 }
+    | {-epsilon-}                 { [] }
+
+assocTypeBind :: { AssocTypeBind }
hunk ./ParserHelper.hs 43
-mkClassInst :: ([Constraint], Type) -> AssocTypeBind -> [ValBind] 
+mkClassInst :: ([Constraint], Type) -> [AssocTypeBind] -> [ValBind] 
hunk ./ParserHelper.hs 45
-mkClassInst (cs, (TyApp (TyConstruct i) t)) assoc vals = 
-    ClassInst i t cs assoc vals
+mkClassInst (cs, (TyApp (TyConstruct i) t)) assocs vals = 
+    ClassInst i t cs assocs vals
hunk ./Symtab.hs 250
-    let -- add the assoc type definition
+    let -- add the assoc type definitions
hunk ./Symtab.hs 252
-        assoc = inst_typeBind ci
-        left = AssocType (assocBind_name assoc) 
-                 (assocBind_index assoc : map TyVar (assocBind_params assoc))
-        right = assocBind_def assoc
-    in modify $ addInstance (EqScheme quants (EqConstraint left right))
-    where addInstance eq s = 
+        eqs = map mkEqConstraint (inst_typeBinds ci)
+    in modify $ addInstance (map (EqScheme quants) eqs)
+    where addInstance eqs s = 
hunk ./Symtab.hs 261
-                        eqEnv = eq : (eqEnv s) }
-
+                        eqEnv = eqs ++ (eqEnv s) }
+          mkEqConstraint assoc =
+              let left = AssocType (assocBind_name assoc) 
+                           (assocBind_index assoc : 
+                            map TyVar (assocBind_params assoc))
+                  right = assocBind_def assoc
+                  in EqConstraint left right
hunk ./SyntaxTransformation.hs 132
-rw_classinst (ClassInst name param constrs tyBind valBinds) =
+rw_classinst (ClassInst name param constrs tyBinds valBinds) =
hunk ./SyntaxTransformation.hs 138
-       tyBind' <- rw_assocTypeBind tyBind
+       tyBinds' <- mapM rw_assocTypeBind tyBinds
hunk ./SyntaxTransformation.hs 141
-       return (AS.ClassInst uid param' constrs' tyBind' valBinds')
+       return (AS.ClassInst uid param' constrs' tyBinds' valBinds')
hunk ./TypeInference.hs 22
+import WellFormedness ( checkTypeScheme )
hunk ./TypeInference.hs 231
+       debug ("first checking if user-supplied signature is well-formed")
+       liftST $ checkTypeScheme [] sc
hunk ./TypeInference.hs 386
-          then panic ("Non-empty set of constraints after type inference:\n" ++
-                      dumpAssumps as ++ "\n" ++ dumpConstraints ps)
+          then phasefail ("deferred constraints left after type inference:\n" ++
+                          dumpAssumps as ++ "\n" ++ dumpConstraints ps ++
+                         "\npossible reason: monomorphism restriction applied "
+                         ++ "to a top-level binding")
hunk ./TypeInference.hs 400
-                 info ("checking types of method implementations")
hunk ./TypeInference.hs 417
-              mapM_ (checkMethod as ci) (inst_valBinds ci)
+              do info ("checking methods of instance `" ++
+                       show (ppr (inst_class ci) <+> 
+                                 pprPrec maxPrec (inst_type ci)) ++ "'")
+                 mapM_ (checkMethod as ci) (inst_valBinds ci)
hunk ./Unification.hs 7
+  matchType, normalise,
hunk ./Unification.hs 30
--- matchType l t1 t2 tries to find a substitution s with 
+matchType :: Type -> Type -> ST (Maybe TypeSubst)
+matchType t1 t2 = 
+    matchType' (freeTypeVarsList t1) t1 t2
+
+matchTypes :: [Type] -> [Type] -> ST (Maybe TypeSubst)
+matchTypes ts1 ts2 = 
+    let frees = Set.unions (map freeTypeVars ts1)
+        in matchTypes' (Set.toList frees) ts1 ts2
+
+-- matchType' l t1 t2 tries to find a substitution s with 
hunk ./Unification.hs 42
-matchType :: [TypeVarId] -> Type -> Type -> ST (Maybe TypeSubst)
-matchType allowed t1@(TyApp l r) t2@(TyApp l' r') =
-    do sl <- matchType allowed l l'
-       sr <- matchType allowed r r'
+matchType' :: [TypeVarId] -> Type -> Type -> ST (Maybe TypeSubst)
+matchType' allowed t1@(TyApp l r) t2@(TyApp l' r') =
+    do sl <- matchType' allowed l l'
+       sr <- matchType' allowed r r'
hunk ./Unification.hs 50
-matchType allowed (TyVar u) t | u `elem` allowed
+matchType' allowed (TyVar u) t | u `elem` allowed
hunk ./Unification.hs 56
-matchType _ (TyVar u) (TyVar u') | u == u'= return $ Just nullSubst
-matchType _ (TyConstruct id) (TyConstruct id') | id == id' 
+matchType' _ (TyVar u) (TyVar u') | u == u'= return $ Just nullSubst
+matchType' _ (TyConstruct id) (TyConstruct id') | id == id' 
hunk ./Unification.hs 59
-matchType allowed (TyAssoc (AssocType id params))
+matchType' allowed (TyAssoc (AssocType id params))
hunk ./Unification.hs 61
-    = matchTypes allowed params params'
-matchType _ t1 t2 = return Nothing
+    = matchTypes' allowed params params'
+matchType' _ t1 t2 = return Nothing
hunk ./Unification.hs 64
-matchTypes :: [TypeVarId] -> [Type] -> [Type] -> ST (Maybe TypeSubst)
-matchTypes allowed t1s t2s = 
-    do substs <- mapM (uncurry $ matchType allowed) (zip t1s t2s)
+matchTypes' :: [TypeVarId] -> [Type] -> [Type] -> ST (Maybe TypeSubst)
+matchTypes' allowed t1s t2s = 
+    do substs <- mapM (uncurry $ matchType' allowed) (zip t1s t2s)
hunk ./Unification.hs 113
---reductionFailed succ err = catchUF succ [ReductionFailed] (\_ -> err)
-
hunk ./Unification.hs 159
-                   subst <- matchTypes freshs
+                   subst <- matchTypes' freshs
hunk ./Unification.hs 173
+
+
+--
+-- Normalisation (multi-step reduction)
+--
+
+normalise :: Type -> UF Type
+normalise t = 
+    do x <- reduceOneStep t
+       case x of
+         Nothing -> return t
+         Just t' -> normalise t'
hunk ./Unification.hs 232
+
+
+--
+-- 1-step matching
+--
+
+matchOneStep :: TypeEq -> UF (Maybe UFResult')
+-- rule refl_U
+matchOneStep (t1 :=: t2) | t1 == t2 = return $ Just (emptyEqs, nullSubst)
+-- rule var_U with symm_U
+matchOneStep (TyVar u :=: t) = oneStepVar u t
+-- rule app_U
+matchOneStep (TyApp l r :=: TyApp l' r') = 
+    return $ Just ([l :=: l', r :=: r'], nullSubst)
+-- rule red_U with symm_U
+matchOneStep (t1@(TyAssoc _) :=: t2@(TyAssoc _)) =
+    do res <- oneStepAssoc t1 t2
+       case res of
+         Nothing -> oneStepAssoc t2 t1
+         Just x -> return $ Just x
+matchOneStep (t1@(TyAssoc _) :=: t2) = oneStepAssoc t1 t2
+matchOneStep (t2 :=: t1@(TyAssoc _)) = oneStepAssoc t1 t2
+-- default
+matchOneStep (t1 :=: t2) = return Nothing
+
hunk ./WellFormedTypes.hs 1
-module WellFormedTypes where
rmfile ./WellFormedTypes.hs
hunk ./WellFormedness.hs 21
-module WellFormedProgram where
-
--- ICFP draft, section 5.1
+module WellFormedness where
hunk ./WellFormedness.hs 33
+import Entailment ( entail )
hunk ./WellFormedness.hs 39
+       mapM checkMethodTypeSchemes classDecs
+       mapM checkAssocTypeDefs classInsts
+       return ()
+
+-- type schemes in method signature must be well-formed
+-- {invalid_method_sig.mhs}
+checkMethodTypeSchemes :: ClassDec -> ST ()
+checkMethodTypeSchemes cdec = 
+    let cid = class_name cdec
+        c = CC $ ClassConstraint cid (TyVar $ class_param cdec)
+        in do debug ("checking method signatures in " ++ showPpr' cid)
+              mapM (checkTypeScheme [c]) (map snd (class_vsigs cdec))
+              return ()
+
+-- associated type definitions must be well-formed
+-- {invalid_assoc_type_def.mhs}
+checkAssocTypeDefs :: ClassInst -> ST ()
+checkAssocTypeDefs ci = 
+    do debug ("checking associated type definitions in instance of class " ++
+              showPpr' (inst_class ci) ++ " for type " ++ 
+              showPpr' (inst_type ci))
+       let rhss = map assocBind_def (inst_typeBinds ci)
+       mapM (checkType (inst_constraints ci)) rhss
hunk ./WellFormedness.hs 66
--- FIXME: need symbol table and unification
hunk ./WellFormedness.hs 174
-checkInstanceDec ci@(ClassInst clazz ty constrs tyBind methodBinds) = 
+checkInstanceDec ci@(ClassInst clazz ty constrs tyBinds methodBinds) = 
hunk ./WellFormedness.hs 180
-       checkAssocTypeHead ci tyBind
-       checkAssocTypeDefinition tyBind
+       mapM (checkAssocTypeHead ci) tyBinds
+       mapM checkAssocTypeDefinition tyBinds
hunk ./WellFormedness.hs 231
-checkIfAllAssocTypesAreDefined (ClassInst classId _ _ tyBind _) = 
+checkIfAllAssocTypesAreDefined (ClassInst classId _ _ tyBinds _) = 
hunk ./WellFormedness.hs 233
-       if length (class_tsigs clazz) /= 1
+       if length (class_tsigs clazz) /= (length tyBinds)
hunk ./WellFormedness.hs 237
-       let classTId = fst $ (class_tsigs clazz)!!0
-       if classTId /= assocBind_name tyBind
+       let sigNames = List.sort $ map fst (class_tsigs clazz)
+           bindNames = List.sort $ map assocBind_name tyBinds
+       if sigNames /= bindNames
hunk ./WellFormedness.hs 241
-                          showPpr classId ++ ": type synonyms do not match")
+                          showPpr classId ++ 
+                          ": type synonyms do not match")
hunk ./WellFormedness.hs 390
+
+
+----------------------
+-- checks for types --
+----------------------
+
+-- the `Theta |- tau' relation in figure 2.
+
+-- checkTypeScheme uses the program's class and equality constraints 
+-- implicitly, i.e. `checkTypeScheme cs t' checks if type scheme t is
+-- well-formed wrt the program constraints and the constraints cs.
+-- FIXME: The constraints cs are not quantified (I simple assume an empty
+-- quantifier list).
+checkTypeScheme :: [Constraint] -> TypeScheme -> ST ()
+checkTypeScheme cs sc@(TypeScheme quants (QualifiedType cs' t)) = 
+    do -- first ensure that no quantifiers is free in the environment
+       -- for computing the free variables of the program environment, we
+       -- only have to consider equality constraints (class constraints
+       -- do not have free variables)
+       eqEnv <- getEqEnv
+       let frees = freeTypeVars eqEnv `Set.union` freeTypeVars cs
+           inters = Set.fromList quants `Set.intersection` frees
+       if not $ Set.null inters
+          then phasefail ("Type scheme " ++ showPpr' sc ++ " is not well-formed"
+                          ++ ": it quantifies over some variables contained in "
+                          ++ "the environment: " ++ 
+                          showCommaListed (Set.toList inters))
+          else return ()
+       checkType (cs ++ cs') t
hunk ./WellFormedness.hs 420
+checkType :: [Constraint] -> Type -> ST ()
+checkType _ (TyVar _) = return ()
+checkType cs (TyApp t1 t2) = 
+    do checkType cs t1
+       checkType cs t2
+checkType _ (TyConstruct _) = return ()
+checkType cs at@(TyAssoc (AssocType id params)) = 
+    do mapM (checkType cs) params
+       cd <- findClassOfAssocType id
+       let c = case params of
+                 [] -> panic ("empty argument list for associated type " ++ 
+                              showPpr' id)
+                 (t:_) -> CC $ ClassConstraint (class_name cd) t           
+       e <- entail cs c
+       if not e
+          then phasefail ("illegal associated type application: " ++
+                          showPpr' at ++ ". Cannot deduce " ++ showPpr' c
+                          ++ " from program context and " ++
+                          showCommaListed cs)
+          else return ()
hunk ./tests/driver/check 67
+$failed = "";
hunk ./tests/driver/check 113
+
hunk ./tests/driver/check 153
-                        
+
hunk ./tests/driver/check 192
+               $failed .= "tests/$phase/$leaf/$source\n";
hunk ./tests/driver/check 248
+
+print "\n\n";
+print "Tests that failed:\n";
+print "------------------\n\n";
+print $failed;
addfile ./tests/type-inference/should_fail/014.err
hunk ./tests/type-inference/should_fail/014.err 1
+type error while checking explicitly typed binding `foo'
+  infered signature: forall v[-1] . v[-1] -> v[-1]
+  user-supplied signature: Int -> T Int
addfile ./tests/type-inference/should_fail/014.mhs
hunk ./tests/type-inference/should_fail/014.mhs 1
+class C a where {
+  type T a;
+  foo :: a -> T a;
+}
+
+instance C Int where {
+  type T Int = Bool;
+  foo x = x;
+}
addfile ./tests/type-inference/should_fail/015.err
hunk ./tests/type-inference/should_fail/015.err 1
+Cannot unify {v[-22] -> Int = E Int -> v[-27], T v[-22] = Int}. Unsatisfiable equality constraint: Bool = Int
addfile ./tests/type-inference/should_fail/015.mhs
hunk ./tests/type-inference/should_fail/015.mhs 1
+data E t = E t;
+
+class C a where {
+  type T a;
+  foo :: a -> T a;
+}
+
+instance C Int where {
+  type T Int = Bool;
+  foo x = x == 1;
+}
+
+instance C Bool where {
+  type T Bool = Int;
+  foo x = if x then 1 else 0;
+}
+
+instance C t => C (E t) where {
+  type T (E t) = T t;
+  foo x = case x of
+            E y -> foo y;
+  ;
+}
+
+f x = foo x + 42;
+
+g = (f True, f (E 1));
addfile ./tests/type-inference/should_fail/016.err
hunk ./tests/type-inference/should_fail/016.err 1
+illegal associated type application: `T a[1]'. Cannot deduce `C a[1]' from program context and {}
addfile ./tests/type-inference/should_fail/016.mhs
hunk ./tests/type-inference/should_fail/016.mhs 1
+class C a where {
+  type T a;
+}
+
+foo :: a -> T a;
+foo = foo;
addfile ./tests/type-inference/should_fail/017.err
hunk ./tests/type-inference/should_fail/017.err 1
+deferred constraints left after type inference:
+{Assumptions: {bar = v[-2] -> T v[-2], foo = forall b . D b => b -> T b}}
+{Constraints: {D v[-2]}}
+possible reason: monomorphism restriction applied to a top-level binding
addfile ./tests/type-inference/should_fail/017.mhs
hunk ./tests/type-inference/should_fail/017.mhs 1
+class C a where {
+  type T a;
+}
+
+class C b => D b where {
+  foo :: b -> T b;
+}
+
+bar = foo;
addfile ./tests/type-inference/should_pass/026.mhs
hunk ./tests/type-inference/should_pass/026.mhs 1
+data E t = E t;
+
+class C a where {
+  type T a;
+  foo :: a -> T a;
+}
+
+instance C Int where {
+  type T Int = Bool;
+  foo x = x == 1;
+}
+
+instance C Bool where {
+  type T Bool = Bool;
+  foo x = x;
+}
+
+instance C t => C (E t) where {
+  type T (E t) = T t;
+  foo x = case x of
+            E y -> foo y;
+  ;
+}
+
addfile ./tests/type-inference/should_pass/026.out
addfile ./tests/type-inference/should_pass/027.mhs
hunk ./tests/type-inference/should_pass/027.mhs 1
+data E t = E t;
+
+class C a where {
+  type T a;
+  foo :: a -> T a;
+}
+
+instance C Int where {
+  type T Int = Bool;
+  foo x = x == 1;
+}
+
+instance C Bool where {
+  type T Bool = Int;
+  foo x = if x then 1 else 0;
+}
+
+instance C t => C (E t) where {
+  type T (E t) = T t;
+  foo x = case x of
+            E y -> foo y;
+  ;
+}
+
+f x = foo x + 42;
+
+g = (f True, f (E False));
addfile ./tests/type-inference/should_pass/027.out
hunk ./tests/type-inference/should_pass/027.out 1
+f :: forall v[-2] . T v[-2] = Int, C v[-2] => v[-2] -> Int
+g :: (Int, Int)
addfile ./tests/type-inference/should_pass/028.mhs
hunk ./tests/type-inference/should_pass/028.mhs 1
+class C a where {
+  type T a;
+}
+
+class C b => D b where {
+  foo :: b -> T b;
+}
+
+bar x = foo x;
addfile ./tests/type-inference/should_pass/028.out
hunk ./tests/type-inference/should_pass/028.out 1
+bar :: forall v[-2] . D v[-2] => v[-2] -> T v[-2]
addfile ./tests/type-inference/should_pass/029.mhs
hunk ./tests/type-inference/should_pass/029.mhs 1
-
+data D x = D x;
+
+class C a where {
+  type T a;
+}
+
+instance C x => C (D x) where {
+  type T (D x) = T x;
+}
+
+foo :: C a => a -> T a;
+foo = foo;
addfile ./tests/type-inference/should_pass/029.out
hunk ./tests/type-inference/should_pass/029.out 1
+foo :: forall a[1] . C a[1] => a[1] -> T a[1]
addfile ./tests/type-inference/should_pass/030.mhs
hunk ./tests/type-inference/should_pass/030.mhs 1
+class C a where {
+  type T a;
+  type S a;
+  foo :: a -> T a -> S a;
+}
+
+instance C Int where {
+  type T Int = Int;
+  type S Int = Int -> Bool;
+  foo i j k = i + j == k;
+}
+
+--bar :: C a, T a = S a => a -> T a -> S a;
+bar a t = foo a (foo a t);
addfile ./tests/type-inference/should_pass/030.out
hunk ./tests/type-inference/should_pass/030.out 1
+bar :: forall v[-2] . T v[-2] = S v[-2], C v[-2] => v[-2] -> T v[-2] -> S v[-2]
addfile ./tests/well-formed/should_fail/invalid_assoc_type_def.err
hunk ./tests/well-formed/should_fail/invalid_assoc_type_def.err 1
+illegal associated type application: `T x[1]'. Cannot deduce `C x[1]' from program context and {}
addfile ./tests/well-formed/should_fail/invalid_assoc_type_def.mhs
hunk ./tests/well-formed/should_fail/invalid_assoc_type_def.mhs 1
+data D x = D x;
+
+class C a where {
+  type T a;
+}
+
+instance C (D x) where {
+  type T (D x) = T x;
+}
addfile ./tests/well-formed/should_fail/invalid_method_sig.err
hunk ./tests/well-formed/should_fail/invalid_method_sig.err 1
+illegal associated type application: `T b'. Cannot deduce `C b' from program context and {C a}
addfile ./tests/well-formed/should_fail/invalid_method_sig.mhs
hunk ./tests/well-formed/should_fail/invalid_method_sig.mhs 1
+class C a where {
+  type T a;
+  foo :: a -> b -> T b;
+}
hunk ./tests/well-formed/should_fail/missing_assoc_type2.err 1
-Parser error, next tokens: 
-  line 12:3, ReservedIdT "type"
-  line 12:8, ConIdT "U"
-  line 12:10, ConIdT "Int"
+illegal instance declaration for class C: type synonyms do not match
}