[fix right sections, fix constructor typing
John Meacham <john@repetae.net>**20060210064205] hunk ./FrontEnd/Tc/Main.hs 4
+import List
hunk ./FrontEnd/Tc/Main.hs 120
-    e2 <- tiExpr e2 (arg `fn` (arg2 `fn` typ))
-    e1 <- tiExpr e1 arg2
+    ret <- newBox Star
+    e1 <- tcExpr e1 arg2
+    e2 <- tcExpr e2 (arg `fn` (arg2 `fn` ret))
+    (arg `fn` ret) `subsumes` typ
hunk ./FrontEnd/Tc/Main.hs 158
-            varBind mv (b1 `fn` b2)
+            --varBind mv (b1 `fn` b2)
+            boxyMatch (TMetaVar mv) (b1 `fn` b2)
hunk ./FrontEnd/Tc/Main.hs 172
-        lamPoly ps e s@TBox {} rs = lam ps e s rs
hunk ./FrontEnd/Tc/Main.hs 285
-        v `boxyMatch` typ
+        --v `boxyMatch` typ
+        typ `subsumes` v
hunk ./FrontEnd/Tc/Main.hs 292
-    t `boxyMatch` typ
+    typ `subsumes` t -- `boxyMatch` typ
hunk ./FrontEnd/Tc/Main.hs 310
-    s `boxyMatch` (foldr fn typ bs)
+    --s `boxyMatch` (foldr fn typ bs)
+    s `subsumes` (foldr fn typ bs)
hunk ./FrontEnd/Tc/Main.hs 318
-    TAp tList v `boxyMatch` typ
+    --TAp tList v `boxyMatch` typ
+    typ `subsumes` TAp tList v
hunk ./FrontEnd/Tc/Main.hs 326
-    TAp tList v `boxyMatch` typ
+    --TAp tList v `boxyMatch` typ
+    typ `subsumes` TAp tList v
hunk ./FrontEnd/Tc/Main.hs 359
+    liftIO $ mapM_ putStrLn $ sort [ show x ++ "  " ++ prettyPrintType y | (x,y) <- nenv]
hunk ./FrontEnd/Tc/Main.hs 407
-            varBind mv (b1 `fn` b2)
+            --varBind mv (b1 `fn` b2)
+            (TMetaVar mv) `boxyMatch`  (b1 `fn` b2)
hunk ./FrontEnd/Tc/Main.hs 414
-            liftIO $ print (p',env)
+            --liftIO $ print (p',env)
hunk ./FrontEnd/Tc/Main.hs 441
-    sc <- freshSigma sc
-    case sc of
-        TForAll _ (_ :=> t) -> tcDecl decl t
-        t -> tcDecl decl t
+    --sc <- freshSigma sc
+    (_,typ) <- skolomize sc
+    tcDecl decl typ
+    --case sc of
+    --    TForAll _ (_ :=> t) -> tcDecl decl t
+    --    t -> tcDecl decl t
hunk ./FrontEnd/Tc/Monad.hs 330
-            Just r -> error $ "varBind: binding unfree: " ++ tupled [pprint u,prettyPrintType tt,prettyPrintType r]
+            Just r -> fail $ "varBind: binding unfree: " ++ tupled [pprint u,prettyPrintType tt,prettyPrintType r]
hunk ./FrontEnd/Tc/Unify.hs 33
+        printRule "SKOL"
hunk ./FrontEnd/Tc/Unify.hs 40
+        printRule "SPEC"
hunk ./FrontEnd/Tc/Unify.hs 112
-        a <- newBox (kind s1)
-        b <- newBox (kind s2)
+        a <- newMetaVar Tau (kind s1)
+        b <- newMetaVar Tau (kind s2)
hunk ./FrontEnd/Tc/Unify.hs 125
+
+
hunk ./FrontEnd/Tc/Unify.hs 129
-    bm a (TMetaVar mv) | (TCon ca,as) <- fromTAp a = do
-        bs <- mapM (newBox . kind) as
-        a `boxyMatch` foldl TAp (TCon ca) bs
-        varBind mv (foldl TAp (TCon ca) bs)
-        return False
+    --bm a (TMetaVar mv) | (TCon ca,as) <- fromTAp a = do
+    --    varBind mv a
+    --    return False
+        --bs <- mapM (newBox . kind) as
+        --a `boxyMatch` foldl TAp (TCon ca) bs
+        --varBind mv (foldl TAp (TCon ca) bs)
+        --return False
hunk ./FrontEnd/Tc/Unify.hs 149
-    -- XXX app
-    bm a b | (t1,as1@(_:_)) <- fromTAp a, (t2,as2) <- fromTAp b = case sameLength as1 as2 of
-        False -> unificationError a b
-        True -> do
-            t1 `boxyMatch` t2
-            sequence_ [boxyMatch x y | x <- as1 | y <- as2] >> return False
-            printRule "XXX Apps"
-            return False
+
hunk ./FrontEnd/Tc/Unify.hs 169
+    bm a (TMetaVar mv)  = do
+        varBind mv a
+        return False
+    --bm (TMetaVar mv) b  = do
+    --    varBind mv b
+    --    return False
hunk ./FrontEnd/Tc/Unify.hs 176
+    -- XXX app
+    bm a b | (t1,as1@(_:_)) <- fromTAp a, (t2,as2) <- fromTAp b = case sameLength as1 as2 of
+        False -> unificationError a b
+        True -> do
+            t1 `boxyMatch` t2
+            sequence_ [boxyMatch x y | x <- as1 | y <- as2] >> return False
+            printRule "XXX Apps"
+            return False