[handle metavars properly in subsumption. move unifier into Tc/Monad
John Meacham <john@repetae.net>**20051209133458] hunk ./FrontEnd/Tc/Main.hs 51
-    t <- br >>= findType
+    t <- br
hunk ./FrontEnd/Tc/Main.hs 57
-tiExprPoly e t@TBox {} = tiExpr e t
-tiExprPoly e t = do
-    t' <- freshInstance t
-    tiExpr e t'
+tiExprPoly e t@TBox {} = tiExpr e t   -- GEN2
+tiExprPoly e t = do                   -- GEN1
+    -- (_,t) <- skolomize t
+    tiExpr e t
hunk ./FrontEnd/Tc/Main.hs 126
-            s1 <- rs1 >>= findType
-            s2 <- rs2 >>= findType
+            s1 <- rs1
+            s2 <- rs2
hunk ./FrontEnd/Tc/Main.hs 133
-            s1 <- br >>= findType
+            s1 <- br
hunk ./FrontEnd/Tc/Main.hs 143
-            s <- freshInstance s
+            --(_,s) <- skolomize s
hunk ./FrontEnd/Tc/Main.hs 188
+    rr <- flattenType rr
hunk ./FrontEnd/Tc/Monad.hs 18
+    varBind,
hunk ./FrontEnd/Tc/Monad.hs 30
+import Control.Monad.Error
hunk ./FrontEnd/Tc/Monad.hs 49
-import Type(mgu,tv)
+import Type(tv)
hunk ./FrontEnd/Tc/Monad.hs 110
-{-
-runTI :: Map.Map Name Scheme-> ClassHierarchy -> KindEnv -> SigEnv -> Module -> TI a -> IO a
-runTI env' ch' kt' st' mod' (TI tim) = do
-    vn <- newIORef 0
-    runReaderT tim tcenv {  tcVarnum = vn } where
-    tcenv = TcEnv {
-        tcClassHierarchy = ch',
-        tcKinds = kt',
-        tcModuleName = mod',
-        tcSigs = st',
-        tcVarnum = undefined,
-        tcDConsEnv = env',
-        tcDiagnostics = [Msg Nothing $ "Compilation of module: " ++ fromModule mod']
-        }
--}
hunk ./FrontEnd/Tc/Monad.hs 152
-        Just u -> return () -- extSubst u
-        Nothing -> do
+        Nothing -> return ()
+        Just err -> do
hunk ./FrontEnd/Tc/Monad.hs 158
-                                           pretty t2')
+                                           pretty t2' ++ "\n" ++ err)
hunk ./FrontEnd/Tc/Monad.hs 172
-    return (liftIO $ readIORef r, TBox k u r)
+    return (liftIO $ readIORef r >>= flattenType, TBox k u r)
+
+mgu     :: (MonadIO m) => Type -> Type -> m (Maybe String)
hunk ./FrontEnd/Tc/Monad.hs 176
+mgu x y = do
+    r <- runErrorT (mgu'' x y)
+    case r of
+        Right _ -> return Nothing
+        Left (err::String) -> return (Just err)
+mgu'' x y = do
+    x' <- findType x
+    y' <- findType y
+    mgu' x' y'
+mgu' (TAp l r) (TAp l' r')
+   = do s1 <- mgu'' l l'
+        s2 <- mgu'' r r'
+        return ()
+mgu' (TArrow l r) (TArrow l' r')
+   = do s1 <- mgu'' l l'
+        s2 <- mgu'' r r'
+        return ()
+mgu' (TVar u) t | isMetaTV u  = varBind u t
+mgu' t (TVar u) | isMetaTV u  = varBind u t
+mgu' (TVar a) (TVar b) | a == b = return ()
+mgu' c1@(TCon tc1) c2@(TCon tc2)
+           | tc1==tc2 = return ()
+           | otherwise = fail $ "mgu: Constructors don't match:" ++ show (c1,c2)
+mgu' TForAll {} _ = error "attempt to unify TForall"
+mgu' _ TForAll {} = error "attempt to unify TForall"
+mgu' _ TBox {} = error "attempt to unify TBox"
+mgu' TBox {} _ = error "attempt to unify TBox"
+mgu' t1 t2  = fail $ "mgu: types do not unify:" ++ show (t1,t2)
hunk ./FrontEnd/Tc/Monad.hs 315
-skolomize s = freshSigma s >>= \x -> case x of
+skolomize s@TForAll {} = freshSigma s >>= \x -> case x of
hunk ./FrontEnd/Tc/Monad.hs 317
+    r -> return ([],r)
+skolomize s = return ([],s)
hunk ./FrontEnd/Tc/Monad.hs 341
-        f t _ = error $ "boxySpec: " ++ show t
+        f t _ = return t
+        -- f t _ = error $ "boxySpec: " ++ show t
hunk ./FrontEnd/Tc/Monad.hs 347
-{-
-newSigma :: Sigma -> Tc ([Tyvar],Rho)
-newSigma (TForAll vs qt) = do
-    nvs <- mapM (newVar . tyvarKind) vs
-    return (nvs,inst (Map.fromList $ zip (map tyvarAtom vs) (map TVar nvs)) qt)
-newSigma x = return ([],x)
-
-freshInst :: Scheme -> TI (Qual Type)
-freshInst (Forall ks qt) = do
-        ts <- mapM newTVar ks
-        let v = (inst ts qt)
-        return (v)
--}
hunk ./FrontEnd/Tc/Monad.hs 350
-    freshSigma (TForAll (tv r) ([] :=> r))
+    let mtvs = (filter isMetaTV (tv r))
+    nvs <- mapM (newVar . tyvarKind) [ t | t <- mtvs]
+    sequence_ [ varBind mv (TVar v) | v <- nvs |  mv <- mtvs ]
+    freshSigma (tForAll nvs ([] :=> r))
hunk ./FrontEnd/Tc/Monad.hs 355
+varBind :: (MonadIO m) => Tyvar -> Type -> m ()
+varBind u t | not (isMetaTV u) = error "varBind: not metatv"
+            | t == TVar u   = return ()
+            | u `elem` tv t = fail "varBind: occurs check fails"
+            | kind u == kind t, Just r <- tyvarRef u = do
+                x <- liftIO $ readIORef r
+                case x of
+                    Just r -> fail $ "varBind: bining unfree: " ++ show (u,t,r)
+                    Nothing -> liftIO $ writeIORef r (Just t)
+            | otherwise        = error $ "varBind: kinds do not match:" ++ show (u,t)
hunk ./FrontEnd/Tc/Type.hs 10
+    tv,
hunk ./FrontEnd/Tc/Type.hs 19
-import Type(kind)
+import Type(kind,tv)
hunk ./FrontEnd/Tc/Unify.hs 12
+import Data.IORef
hunk ./FrontEnd/Tc/Unify.hs 27
+    sub (TArrow a b) (TVar t) | isMetaTV t = do
+        a' <- newTVar (kind a)
+        b' <- newTVar (kind b)
+        varBind t (TArrow a' b')
+        (TArrow a b) `subsumes` (TArrow a' b')
+    sub (TAp a b) (TVar t) | isMetaTV t = do
+        a' <- newTVar (kind a)
+        b' <- newTVar (kind b)
+        varBind t (TAp a' b')
+        (TAp a b) `subsumes` (TAp a' b')
+
hunk ./FrontEnd/Tc/Unify.hs 76
-        _ -> fail $ "subsumes failure: " ++ show (a,b)
+        _ -> do
+            a' <- findType a
+            b' <- findType b
+            fail $ "subsumes failure: " ++ show ((a,b),(a',b'))
hunk ./FrontEnd/Tc/Unify.hs 156
+    bm (TArrow a b) (TVar t) | isMetaTV t = do
+        a' <- newTVar (kind a)
+        b' <- newTVar (kind b)
+        varBind t (TArrow a' b')
+        (TArrow a b) `boxyMatch` (TArrow a' b')
+        return False
+    bm (TAp a b) (TVar t) | isMetaTV t = do
+        a' <- newTVar (kind a)
+        b' <- newTVar (kind b)
+        varBind t (TAp a' b')
+        (TAp a b) `boxyMatch` (TAp a' b')
+        return False
hunk ./FrontEnd/Tc/Unify.hs 175
-