[improve boxy type checker, make subsumption fall back on boxy matching
John Meacham <john@repetae.net>**20060210051747] hunk ./FrontEnd/Tc/Monad.hs 50
+import Support.CanType
hunk ./FrontEnd/Tc/Monad.hs 296
+
+-- this removes all boxes, replacing them with tau vars
+unBox ::  Type -> Tc Type
+unBox tv = ft' tv where
+    ft (TAp x y) = liftM2 TAp (ft' x) (ft' y)
+    ft (TArrow x y) = liftM2 TArrow (ft' x) (ft' y)
+    ft t@TCon {} = return t
+    ft (TForAll vs (ps :=> t)) = do
+        when (any isMetaTV vs) $ error "metatv in forall binding"
+        ps' <- sequence [ ft' t >>= return . IsIn c | ~(IsIn c t) <- ps ]
+        t' <- ft' t
+        return $ TForAll vs (ps' :=> t')
+    ft t@(TMetaVar mv)
+        | isBoxyMetaVar mv = do
+            tmv <- newMetaVar Tau (getType mv)
+            varBind mv tmv
+            return tmv
+        | otherwise =  return t
+    ft t | ~(Just tv) <- extractTyVar t  = return (TVar tv)
+    ft' t = findType t >>= ft
+
+
+-- Bind mv to type, first filling in any boxes in type with tau vars
hunk ./FrontEnd/Tc/Monad.hs 321
-    | kind u /= kind t = error $ "varBind: kinds do not match:" ++ show (u,t)
+    | getType u /= getType t = error $ "varBind: kinds do not match:" ++ show (u,t)
hunk ./FrontEnd/Tc/Monad.hs 323
-        (t,be,_) <- unbox t
-        when be $ error $ "binding boxy: " ++ tupled [pprint u,prettyPrintType t]
-        when (u `elem` freeMetaVars t) $ unificationError (TMetaVar u) t -- occurs check
+        tt <- unBox t
+        --(t,be,_) <- unbox t
+        --when be $ error $ "binding boxy: " ++ tupled [pprint u,prettyPrintType t]
+        when (u `elem` freeMetaVars tt) $ unificationError (TMetaVar u) tt -- occurs check
hunk ./FrontEnd/Tc/Monad.hs 330
-            Just r -> error $ "varBind: binding unfree: " ++ tupled [pprint u,prettyPrintType t,prettyPrintType r]
-            Nothing -> liftIO $ writeIORef r (Just t)
+            Just r -> error $ "varBind: binding unfree: " ++ tupled [pprint u,prettyPrintType tt,prettyPrintType r]
+            Nothing -> liftIO $ do
+                putStrLn $ "varBind: " ++ pprint u <+> prettyPrintType t 
+                writeIORef r (Just tt)
+
+
+
+
+zonkBox :: MetaVar -> Tc Type
+zonkBox mv | isBoxyMetaVar mv = findType (TMetaVar mv)
+zonkBox mv = fail $ "zonkBox: nonboxy" ++ show mv
+
+readFilledBox :: MetaVar -> Tc Type
+readFilledBox mv | isBoxyMetaVar mv = zonkBox mv >>= \v -> case v of
+    TMetaVar mv' | mv == mv' -> fail $ "readFilledBox: " ++ show mv
+    t -> return t
+readFilledBox mv = error $ "readFilledBox: nonboxy" ++ show mv
+
+elimBox :: MetaVar -> Tc Type
+elimBox mv | isBoxyMetaVar mv = do
+    t <- readMetaVar mv
+    case t of
+        Just t -> return t
+        Nothing -> newMetaVar Tau (getType mv)
+
+elimBox mv = error $ "elimBox: nonboxy" ++ show mv
+
+
hunk ./FrontEnd/Tc/Type.hs 7
+    followTaus,
hunk ./FrontEnd/Tc/Type.hs 9
+    readMetaVar,
hunk ./FrontEnd/Tc/Type.hs 27
+import Support.CanType
hunk ./FrontEnd/Tc/Type.hs 51
+typeOfType :: Type -> (MetaVarType,Bool)
+typeOfType TForAll { typeArgs = as, typeBody = _ :=> t } = (Sigma,isBoxy t)
+typeOfType t | isTau' t = (Tau,isBoxy t)
+typeOfType t = (Rho,isBoxy t)
+
+
hunk ./FrontEnd/Tc/Type.hs 226
+followTaus :: MonadIO m => Type -> m Type
+followTaus tv@(TMetaVar mv@MetaVar {metaRef = r }) | not (isBoxyMetaVar mv) = liftIO $ do
+    rt <- readIORef r
+    case rt of
+        Nothing -> return tv
+        Just t -> do
+            t' <- followTaus t
+            writeIORef r (Just t')
+            return t'
+followTaus tv = return tv
hunk ./FrontEnd/Tc/Type.hs 250
+readMetaVar :: MonadIO m => MetaVar -> m (Maybe Type)
+readMetaVar MetaVar { metaRef = r }  = liftIO $ do
+    rt <- readIORef r
+    case rt of
+        Nothing -> return Nothing
+        Just t -> do
+            t' <- findType t
+            writeIORef r (Just t')
+            return (Just t')
+
+
+
hunk ./FrontEnd/Tc/Type.hs 301
+
+instance CanType MetaVar Kind where
+    getType mv = metaKind mv
+
+instance CanType Type Kind where
+    getType = kind
+
+instance CanType Tycon Kind where
+    getType = kind
+
+instance CanType Tyvar Kind where
+    getType = kind
+
+
+
hunk ./FrontEnd/Tc/Unify.hs 14
-    {-
-aquireType :: Sigma' -> Tc Sigma'
-aquireType s = do
-    s <- findType s
-    case s of
-        TBox { typeBox = box } -> do
-            r <- openBox box
-            case r of
-                Just t -> aquireType t
-                Nothing -> return s
-        _ -> return s
- -}
+
+-- | this ensures the first argument is at least as polymorphic as the second
+-- actual/offered <= expected
+-- actual/offered `subsumes` expected
hunk ./FrontEnd/Tc/Unify.hs 21
-    --s1 <- findType s1
-    --s2 <- findType s2
-    (s1,_,_) <- unbox s1
-    (s2,_,_) <- unbox s2
+    s1 <- findType s1
+    s2 <- findType s2
+    --(s1,_,_) <- unbox s1
+    --(s2,_,_) <- unbox s2
hunk ./FrontEnd/Tc/Unify.hs 29
-    sub tb@TMetaVar {} b = boxyMatch tb b
+    sub tb@(TMetaVar mv) b  = boxyMatch tb b
hunk ./FrontEnd/Tc/Unify.hs 57
-    sub t@(TArrow s1 s2) (TMetaVar mv) = do
-        a <- newMetaVar (metaType mv) (kind s1)
-        b <- newMetaVar (metaType mv) (kind s2)
-        subsumes t (a `fn` b)
-        varBind mv (a `fn` b)
+    sub t@(TArrow s1 s2) (TMetaVar mv) | isBoxyMetaVar mv = do
+        mvb <- readMetaVar mv
+        case mvb of
+            Nothing -> do
+                a <- newMetaVar (metaType mv) (kind s1)
+                b <- newMetaVar (metaType mv) (kind s2)
+                subsumes t (a `fn` b)
+                varBind mv (a `fn` b)
+            Just ty -> do
+                boxyMatch t ty
hunk ./FrontEnd/Tc/Unify.hs 70
-    sub a b | isTau a && isTau b = unify a b
+    sub a b = boxyMatch a b
+    --sub a b | isTau a && isTau b = unify a b
+
hunk ./FrontEnd/Tc/Unify.hs 82
-    --s1 <- findType s1
-    --s2 <- findType s2
-    (s1,_,_) <- unbox s1
-    (s2,_,_) <- unbox s2
+    s1 <- findType s1
+    s2 <- findType s2
+    --(s1,_,_) <- unbox s1
+    --(s2,_,_) <- unbox s2
hunk ./FrontEnd/Tc/Unify.hs 143
+    -- 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 171
+{-
hunk ./FrontEnd/Tc/Unify.hs 178
+        -}
hunk ./Options.hs 120
-    , Option ['C'] ["justcheck"] (NoArg  (optMode_s CompileHoGrin))   "Typecheck, compile ho and grin."
-    , Option ['c'] [] (NoArg  (optMode_s CompileHo))   "Typecheck and compile ho."
+    , Option ['C'] []            (NoArg  (optMode_s CompileHoGrin))   "Typecheck, compile ho and grin."
+    , Option ['c'] []            (NoArg  (optMode_s CompileHo))   "Typecheck and compile ho."