[enforce invarient that a boxy type may never appear in the range of a substitution
John Meacham <john@repetae.net>**20051220015943] hunk ./FrontEnd/Tc/Main.hs 3
-import Control.Monad.Error
hunk ./FrontEnd/Tc/Main.hs 4
-import List((\\), intersect, union)
hunk ./FrontEnd/Tc/Main.hs 5
-import qualified Text.PrettyPrint.HughesPJ as PPrint
hunk ./FrontEnd/Tc/Main.hs 13
-import FrontEnd.KindInfer(KindEnv,hsQualTypeToSigma)
+import FrontEnd.KindInfer
hunk ./FrontEnd/Tc/Main.hs 54
-    (_,t) <- skolomize t
+    --(_,t) <- skolomize t
hunk ./FrontEnd/Tc/Main.hs 61
-    tiExpr e t
+    e <- tiExpr e t
+    (_,False,_) <- unbox t
+    return e
hunk ./FrontEnd/Tc/Main.hs 68
-    sc <- freshSigma sc
+--    sc <- freshSigma sc
hunk ./FrontEnd/Tc/Main.hs 75
-    sc <- freshSigma sc
+--    sc <- freshSigma sc
hunk ./FrontEnd/Tc/Main.hs 82
-    t `subsumes` typ
+    t `boxyMatch` typ
hunk ./FrontEnd/Tc/Main.hs 91
+{-
hunk ./FrontEnd/Tc/Main.hs 103
-
+ -}
hunk ./FrontEnd/Tc/Main.hs 154
+            l' <- lam (p:ps) e (b1 `fn` b2) rs
hunk ./FrontEnd/Tc/Main.hs 156
-            lam (p:ps) e (b1 `fn` b2) rs
+            return l'
hunk ./FrontEnd/Tc/Main.hs 170
-            (_,s) <- skolomize s
+            --(_,s) <- skolomize s
hunk ./FrontEnd/Tc/Main.hs 282
-        v `subsumes` typ
+        v `boxyMatch` typ
hunk ./FrontEnd/Tc/Main.hs 288
-    t `subsumes` typ
+    t `boxyMatch` typ
hunk ./FrontEnd/Tc/Main.hs 306
-    s `subsumes` (foldr fn typ bs)
+    s `boxyMatch` (foldr fn typ bs)
hunk ./FrontEnd/Tc/Main.hs 313
-    TAp tList v `subsumes` typ
+    TAp tList v `boxyMatch` typ
hunk ./FrontEnd/Tc/Main.hs 320
-    TAp tList v `subsumes` typ
+    TAp tList v `boxyMatch` typ
hunk ./FrontEnd/Tc/Main.hs 367
+{-
hunk ./FrontEnd/Tc/Main.hs 372
-
+-}
hunk ./FrontEnd/Tc/Main.hs 376
+    typ <- findType typ
hunk ./FrontEnd/Tc/Main.hs 389
-        matches' <- mapM (`tcMatch` typ) matches
-        return (HsFunBind matches', Map.singleton (getDeclName decl) typ)
+    typ <- findType typ
+    matches' <- mapM (`tcMatch` typ) matches
+    return (HsFunBind matches', Map.singleton (getDeclName decl) typ)
hunk ./FrontEnd/Tc/Main.hs 398
+            l' <- lam (p:ps) (b1 `fn` b2) rs
hunk ./FrontEnd/Tc/Main.hs 400
-            lam (p:ps) (b1 `fn` b2) rs
+            return l'
hunk ./FrontEnd/Tc/Main.hs 403
-            s1' `boxyMatch` box
hunk ./FrontEnd/Tc/Main.hs 404
+            s1' `boxyMatch` box
hunk ./FrontEnd/Tc/Main.hs 416
-            (_,s) <- skolomize s
+            --(_,s) <- skolomize s
hunk ./FrontEnd/Tc/Main.hs 429
-    liftIO $ putStrLn $ "typing expl: " ++ show (getDeclName decl)
+    liftIO $ putStrLn $ "** typing expl: " ++ show (getDeclName decl) ++ " " ++ prettyPrintType sc
hunk ./FrontEnd/Tc/Main.hs 431
-    (_,sc) <- skolomize sc
-    tcDecl decl sc
+    --tcDecl decl sc
+    sc <- freshSigma sc
+    case sc of
+        TForAll _ (_ :=> t) -> tcDecl decl t
+        t -> tcDecl decl t
+    --(_,sc) <- skolomize sc
hunk ./FrontEnd/Tc/Monad.hs 164
-newBox k = do
-    newMetaVar Sigma k
-    --u <- newUniq
-    --r <- liftIO $ newIORef Nothing
-    --return (TBox k u r)
-
-
+newBox k = newMetaVar Sigma k
hunk ./FrontEnd/Tc/Monad.hs 180
-        Just x -> return x
+        Just x -> freshSigma x
hunk ./FrontEnd/Tc/Monad.hs 262
-boxyInstantiate (TForAll as qt) = do
-        bs <- mapM (newBox . tyvarKind) as
-        let mp = Map.fromList $ zip (map tyvarAtom as) bs
-            (ps :=> r) = inst mp qt
-        addPreds ps
-        return r
-boxyInstantiate x = return x
+boxyInstantiate = freshInstance Sigma
hunk ./FrontEnd/Tc/Monad.hs 288
-quantify vs ps r = do
+quantify vs ps r | not $ any isBoxyMetaVar vs = do
hunk ./FrontEnd/Tc/Monad.hs 296
-varBind u t | t == TMetaVar u   = return ()
-            | u `elem` freeMetaVars t = unificationError (TMetaVar u) t -- occurs check
-            | kind u == kind t, r <- metaRef u = do
-                x <- liftIO $ readIORef r
-                case x of
-                    Just r -> error $ "varBind: binding unfree: " ++ tupled [pprint u,prettyPrintType t,prettyPrintType r]
-                    Nothing -> liftIO $ writeIORef r (Just t)
-            | otherwise        = error $ "varBind: kinds do not match:" ++ show (u,t)
+varBind u t
+    | kind u /= kind t = error $ "varBind: kinds do not match:" ++ show (u,t)
+    | otherwise = do
+        (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
+        let r = metaRef u
+        x <- liftIO $ readIORef r
+        case x of
+            Just r -> error $ "varBind: binding unfree: " ++ tupled [pprint u,prettyPrintType t,prettyPrintType r]
+            Nothing -> liftIO $ writeIORef r (Just t)
hunk ./FrontEnd/Tc/Type.hs 48
+{-
hunk ./FrontEnd/Tc/Type.hs 61
+-}
hunk ./FrontEnd/Tc/Type.hs 96
+isBoxyMetaVar MetaVar { metaType = t } = t > Tau
+
hunk ./FrontEnd/Tc/Type.hs 137
-        vo <- newLookupName ['a' .. ] () tyvar
-        return $ atom $ char vo
-    --f t | Just tyvar <- extractMetaTV t = do
-    --    return $ atom $  pprint tyvar
+        vo <- maybeLookupName tyvar
+        case vo of
+            Just c  -> return $ atom $ char c
+            Nothing -> return $ atom $ tshow (tyvarAtom tyvar)
hunk ./FrontEnd/Tc/Type.hs 250
+
+-- returns (new type, any open boxes, any open tauvars)
+unbox :: MonadIO m => Type -> m (Type,Bool,Bool)
+unbox tv = do
+    let 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 = tell ([True],[]) >> return t
+            | otherwise =  tell ([],[True]) >> return t
+        ft t | ~(Just tv) <- extractTyVar t  = return (TVar tv)
+        ft' t = findType t >>= ft
+    (tv,(eb,et)) <- runWriterT (ft' tv)
+    return (tv,or eb, or et)
+
hunk ./FrontEnd/Tc/Unify.hs 29
-    s1 <- findType s1
-    s2 <- findType s2
+    --s1 <- findType s1
+    --s2 <- findType s2
+    (s1,_,_) <- unbox s1
+    (s2,_,_) <- unbox s2
hunk ./FrontEnd/Tc/Unify.hs 39
-{-
-    sub (TArrow a b) t | Just t <- extractMetaVar 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) t | Just t <- extractMetaVar t = do
-        a' <- newTVar (kind a)
-        b' <- newTVar (kind b)
-        varBind t (TAp a' b')
-        (TAp a b) `subsumes` (TAp a' b')
-    sub t (TArrow a b) | Just t <- extractMetaVar t = do
-        a' <- newTVar (kind a)
-        b' <- newTVar (kind b)
-        varBind t (TArrow a' b')
-        (TArrow a' b') `subsumes` (TArrow a b)
-    sub t (TAp a b) | Just t <- extractMetaVar 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 68
-        varBind mv (a `fn` b)
hunk ./FrontEnd/Tc/Unify.hs 69
+        varBind mv (a `fn` b)
hunk ./FrontEnd/Tc/Unify.hs 83
-    s1 <- findType s1
-    s2 <- findType s2
+    --s1 <- findType s1
+    --s2 <- findType s2
+    (s1,_,_) <- unbox s1
+    (s2,_,_) <- unbox s2
hunk ./FrontEnd/Tc/Unify.hs 128
-        varBind mv (foldl TAp (TCon ca) bs)
hunk ./FrontEnd/Tc/Unify.hs 129
+        varBind mv (foldl TAp (TCon ca) bs)
hunk ./FrontEnd/Tc/Unify.hs 149
-        varBind mv (TForAll vs (ps :=> a))
hunk ./FrontEnd/Tc/Unify.hs 150
+        varBind mv (TForAll vs (ps :=> a))
hunk ./FrontEnd/Tc/Unify.hs 208
-mgu (TMetaVar u) t = varBind u t
-mgu t (TMetaVar u) = varBind u t
+mgu (TMetaVar u) t | not $ isBoxyMetaVar u = varBind u t
+mgu t (TMetaVar u) | not $ isBoxyMetaVar u = varBind u t
hunk ./Util/VarName.hs 8
+    maybeLookupName,
hunk ./Util/VarName.hs 44
+maybeLookupName :: (Ord ni, Monad m,Show ni) => ni -> VarNameT nc ni no m (Maybe no)
+maybeLookupName t = VarName $ do
+    (nim,_) <- get
+    case Map.lookup t nim of
+        Just x -> return (Just x)
+        Nothing -> return $ fail $ "lookupName not found: " ++ show t