[use higher ranked metavars for boxes
John Meacham <john@repetae.net>**20051213041625] hunk ./FrontEnd/Representation.hs 34
+    MetaVarType(..),
+    MetaVar(..),
hunk ./FrontEnd/Representation.hs 63
+data MetaVarType = Tau | Rho | Sigma
+             deriving(Data,Typeable,Eq,Ord,Show)
+    {-! derive: GhcBinary !-}
hunk ./FrontEnd/Representation.hs 74
-             deriving(Data,Typeable, Ord, Show)
+           | TMetaVar { metaVar :: MetaVar }
+             deriving(Data,Typeable,Ord,Show)
+    {-! derive: GhcBinary !-}
+
+data MetaVar = MetaVar { metaUniq :: !Int, metaKind :: Kind, metaRef :: (IORef (Maybe Type)), metaType :: MetaVarType } -- ^ used only in typechecker
+             deriving(Data,Typeable,Show)
hunk ./FrontEnd/Representation.hs 82
+instance Eq MetaVar where
+    a == b = metaUniq a == metaUniq b
+
+instance Ord MetaVar where
+    compare a b = compare (metaUniq a) (metaUniq b)
hunk ./FrontEnd/Tc/Main.hs 41
-    e' <- tiExpr e (foldr fn typ bs)
-    as' <- sequence [ tiExprPoly a r | r <- bs | a <- as ]
+    e' <- tcExpr e (foldr fn typ bs)
+    as' <- sequence [ tcExprPoly a r | r <- bs | a <- as ]
hunk ./FrontEnd/Tc/Main.hs 49
-    e1 <- tiExpr e1 (bt `fn` typ)
-    e2 <- tiExprPoly e2 bt  -- TODO Poly
+    e1 <- tcExpr e1 (bt `fn` typ)
+    e2 <- tcExprPoly e2 bt  -- TODO Poly
hunk ./FrontEnd/Tc/Main.hs 53
-tiExprPoly ::  HsExp -> Type ->  Tc HsExp
+tiExprPoly,tcExprPoly ::  HsExp -> Type ->  Tc HsExp
hunk ./FrontEnd/Tc/Main.hs 55
-tiExprPoly e t@TBox {} = tiExpr e t   -- GEN2
+tcExprPoly e t = do
+    t <- findType t
+    tiExprPoly e t
+
+tiExprPoly e t@TMetaVar {} = tcExpr e t   -- GEN2
hunk ./FrontEnd/Tc/Main.hs 62
-    tiExpr e t
+    tcExpr e t
hunk ./FrontEnd/Tc/Main.hs 64
-tiExpr ::  HsExp -> Type ->  Tc HsExp
+tiExpr,tcExpr ::  HsExp -> Type ->  Tc HsExp
+
+tcExpr e t = do
+    t <- findType t
+    tiExpr e t
hunk ./FrontEnd/Tc/Main.hs 91
-    e <- tiExpr e typ
+    e <- tcExpr e typ
hunk ./FrontEnd/Tc/Main.hs 99
-    r <- freshInstance s
-    e' <- tiExpr e r
-    s' <- freshSigma s
-    s' `subsumes` typ
+    s `subsumes` typ
+    e' <- tcExprPoly e s
+    --s'@(TForall _ (ps :=> r)) <- freshSigma s
+    --addPreds ps
+    --e' <- tiExpr e r
+    --s' `subsumes` typ
hunk ./FrontEnd/Tc/Main.hs 147
-        e <- tiExpr e typ
+        e <- tcExpr e typ
hunk ./FrontEnd/Tc/Main.hs 167
-            e' <- tiExpr e typ
+            e' <- tcExpr e typ
hunk ./FrontEnd/Tc/Main.hs 180
-    e <- tiExpr e tBool
-    e1 <- tiExpr e1 typ
-    e2 <- tiExpr e2 typ
+    e <- tcExpr e tBool
+    e1 <- tcExpr e1 typ
+    e2 <- tcExpr e2 typ
hunk ./FrontEnd/Tc/Main.hs 200
-        exps' <- mapM (`tiExpr` v) exps
+        exps' <- mapM (`tcExpr` v) exps
hunk ./FrontEnd/Tc/Main.hs 204
-tiExpr (HsParen e) typ = tiExpr e typ
+tiExpr (HsParen e) typ = tcExpr e typ
hunk ./FrontEnd/Tc/Main.hs 209
-                    (tiExpr newExp typ)
+                    (tcExpr newExp typ)
hunk ./FrontEnd/Tc/Main.hs 211
-{-
hunk ./FrontEnd/Tc/Main.hs 213
-    (rb,tb) <- newBox Star
-    (u',ds) <- listen $ tiExpr u tb
-    rr <- rb >>= findType
-    ds :=> rr <- flattenType (ds :=> rr)
+    tb <- newBox Star
+    tb' <- newTVar Star
+    (u',ds) <- listen $ localEnv (Map.singleton (toName Val x) tb') $ tcExpr u tb
+    tb' `boxyMatch` tb
+    ds :=> rr <- flattenType (ds :=> tb)
hunk ./FrontEnd/Tc/Main.hs 219
-    (ds,rs) <- (Class.split ch tvs ds)
+    --(ds,rs) <- (Class.split ch tvs ds)
hunk ./FrontEnd/Tc/Main.hs 221
-    rr <- quantify tvs rs rr
+    rr <- quantify tvs ds rr
hunk ./FrontEnd/Tc/Main.hs 224
-        tiExpr t typ
+        tcExpr t typ
hunk ./FrontEnd/Tc/Main.hs 226
--}
hunk ./FrontEnd/Tc/Monad.hs 16
+    newMetaVar,
hunk ./FrontEnd/Tc/Monad.hs 152
-    u <- newUniq
-    r <- liftIO $ newIORef Nothing
-    return (TBox k u r)
+    newMetaVar Sigma k
+    --u <- newUniq
+    --r <- liftIO $ newIORef Nothing
+    --return (TBox k u r)
hunk ./FrontEnd/Tc/Monad.hs 176
+newTVar :: Kind -> Tc Type
+newTVar k = newMetaVar Sigma k
+
hunk ./FrontEnd/Tc/Monad.hs 180
-newTVar    :: Kind -> Tc Type
-newTVar k   = do
+newMetaVar :: MetaVarType -> Kind -> Tc Type
+newMetaVar t k = do
hunk ./FrontEnd/Tc/Monad.hs 185
-    let ident = toName TypeVal ('v':show n)
-        v = tyvar ident k (Just r)
-    return $ TVar v
+    return $ TMetaVar MetaVar { metaUniq = n, metaKind = k, metaRef = r, metaType = t }
hunk ./FrontEnd/Tc/Monad.hs 191
-
hunk ./FrontEnd/Tc/Monad.hs 215
-freshInst :: Sigma -> Tc (Qual Type)
-freshInst (TForAll as qt) = do
-        ts <- mapM newTVar (map tyvarKind as)
-        return (inst (Map.fromList $ zip (map tyvarAtom as) ts) qt)
-freshInst x = return ([] :=> x)
-
-freshInstance :: Sigma -> Tc Rho
-freshInstance (TForAll as qt) = do
-    ts <- mapM newTVar (map tyvarKind as)
+freshInstance :: MetaVarType -> Sigma -> Tc Rho
+freshInstance typ (TForAll as qt) = do
+    ts <- mapM (newMetaVar typ) (map tyvarKind as)
hunk ./FrontEnd/Tc/Monad.hs 221
-freshInstance x = return x
+freshInstance _ x = return x
hunk ./FrontEnd/Tc/Monad.hs 283
-quantify :: [MetaTV] -> [Pred] -> Rho -> Tc Sigma
-quantify vs ps r | all isMetaTV vs = do
+quantify :: [MetaVar] -> [Pred] -> Rho -> Tc Sigma
+quantify vs ps r = do
hunk ./FrontEnd/Tc/Monad.hs 286
-    nvs <- mapM (newVar . tyvarKind) [ t | t <- vs]
+    nvs <- mapM (newVar . metaKind) vs
hunk ./FrontEnd/Tc/Monad.hs 291
-varBind :: Tyvar -> Type -> Tc ()
-varBind u t | not (isMetaTV u) = error "varBind: not metatv"
-            | t == TVar u   = return ()
-            | u `elem` freeMetaVars t = unificationError (TVar u) t -- occurs check
-            | kind u == kind t, Just r <- tyvarRef u = do
+varBind :: MetaVar -> Type -> Tc ()
+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
hunk ./FrontEnd/Tc/Type.hs 2
-    findType,
hunk ./FrontEnd/Tc/Type.hs 3
-    kind,
+    HasKind(..),
hunk ./FrontEnd/Tc/Type.hs 5
-    Sigma(),
hunk ./FrontEnd/Tc/Type.hs 6
-    Tau(),
-    Rho(),
+    MetaVar(..),
+    MetaVarType(..),
hunk ./FrontEnd/Tc/Type.hs 24
-import Representation hiding(flattenType)
-import Type(kind)
-import Unparse
hunk ./FrontEnd/Tc/Type.hs 26
+import Representation hiding(flattenType, findType)
+import Type(HasKind(..))
+import Unparse
hunk ./FrontEnd/Tc/Type.hs 63
-isTau TBox {} = False
+isTau TBox {} = error "isTau: Box"
hunk ./FrontEnd/Tc/Type.hs 66
+isTau (TMetaVar MetaVar { metaType = t })
+    | t == Tau = True
+    | otherwise = False
hunk ./FrontEnd/Tc/Type.hs 73
+isTau' TBox {} = error "isTau': Box"
hunk ./FrontEnd/Tc/Type.hs 79
-isBoxy TBox {} = True
+isBoxy TBox {} = error "isBoxy: Box"
+isBoxy (TMetaVar MetaVar { metaType = t }) | t > Tau = True
hunk ./FrontEnd/Tc/Type.hs 98
-extractMetaTV :: Monad m => Type -> m MetaTV
-extractMetaTV (TVar t) | isMetaTV t = return t
-extractMetaTV t = fail $ "not a metaTyVar:" ++ show t
+--extractMetaTV :: Monad m => Type -> m MetaTV
+--extractMetaTV (TVar t) | isMetaTV t = return t
+--extractMetaTV t = fail $ "not a metaTyVar:" ++ show t
hunk ./FrontEnd/Tc/Type.hs 106
+extractMetaVar :: Monad m => Type -> m MetaVar
+extractMetaVar (TMetaVar t)  = return t
+extractMetaVar t = fail $ "not a metaTyVar:" ++ show t
+
+extractBox :: Monad m => Type -> m MetaVar
+extractBox (TMetaVar mv) | metaType mv > Tau  = return mv
+extractBox t = fail $ "not a metaTyVar:" ++ show t
+
hunk ./FrontEnd/Tc/Type.hs 135
-    f t | Just tyvar <- extractMetaTV t = do
-        return $ atom $  pprint tyvar
+    --f t | Just tyvar <- extractMetaTV t = do
+    --    return $ atom $  pprint tyvar
hunk ./FrontEnd/Tc/Type.hs 151
+    f (TMetaVar mv) = return $ atom $ pprint mv
hunk ./FrontEnd/Tc/Type.hs 156
+instance DocLike d => PPrint d MetaVarType where
+    pprint  t = case t of
+        Tau -> char 't'
+        Rho -> char 'r'
+        Sigma -> char 's'
+
+instance DocLike d => PPrint d MetaVar where
+    pprint MetaVar { metaUniq = u, metaKind = k, metaType = t }
+        | Star <- k =  pprint t <> tshow u
+        | otherwise = parens $ pprint t <> tshow u <> text " :: " <> pprint k
+
+
hunk ./FrontEnd/Tc/Type.hs 207
-            ft t | Just tv <- extractMetaTV t = if failEmptyMetaVar opt then fail $ "empty meta var" ++ prettyPrintType t else return (TVar tv)
+            ft t@(TMetaVar _) = if failEmptyMetaVar opt then fail $ "empty meta var" ++ prettyPrintType t else return t
+            --ft t | Just tv <- extractMetaTV t = if failEmptyMetaVar opt then fail $ "empty meta var" ++ prettyPrintType t else return (TVar tv)
hunk ./FrontEnd/Tc/Type.hs 215
-freeMetaVars :: Type -> [MetaTV]
-freeMetaVars t = filter isMetaTV $ allFreeVars t
+findType :: MonadIO m => Type -> m Type
+findType tv@(TMetaVar MetaVar {metaRef = r }) = liftIO $ do
+    rt <- readIORef r
+    case rt of
+        Nothing -> return tv
+        Just t -> do
+            t' <- findType t
+            writeIORef r (Just t')
+            return t'
+findType tv = return tv
+
hunk ./FrontEnd/Tc/Type.hs 237
+freeMetaVars :: Type -> [MetaVar]
+freeMetaVars (TVar u)      = []
+freeMetaVars (TAp l r)     = freeMetaVars l `union` freeMetaVars r
+freeMetaVars (TArrow l r)  = freeMetaVars l `union` freeMetaVars r
+freeMetaVars TCon {}       = []
+freeMetaVars TBox {}       = []
+freeMetaVars (TMetaVar mv) = [mv]
+freeMetaVars typ | ~(TForAll vs (_ :=> t)) <- typ = freeMetaVars t
+
hunk ./FrontEnd/Tc/Unify.hs 14
-
+    {-
hunk ./FrontEnd/Tc/Unify.hs 25
-
+ -}
hunk ./FrontEnd/Tc/Unify.hs 29
-    s1 <- aquireType s1
-    s2 <- aquireType s2
+    s1 <- findType s1
+    s2 <- findType s2
hunk ./FrontEnd/Tc/Unify.hs 35
-    sub tb@TBox {} b = boxyMatch tb b
+    sub tb@TMetaVar {} b = boxyMatch tb b
hunk ./FrontEnd/Tc/Unify.hs 37
-    sub (TArrow a b) t | Just t <- extractMetaTV t = do
+{-
+    sub (TArrow a b) t | Just t <- extractMetaVar t = do
hunk ./FrontEnd/Tc/Unify.hs 43
-    sub (TAp a b) t | Just t <- extractMetaTV t = do
+    sub (TAp a b) t | Just t <- extractMetaVar t = do
hunk ./FrontEnd/Tc/Unify.hs 48
-    sub t (TArrow a b) | Just t <- extractMetaTV t = do
+    sub t (TArrow a b) | Just t <- extractMetaVar t = do
hunk ./FrontEnd/Tc/Unify.hs 53
-    sub t (TAp a b) | Just t <- extractMetaTV t = do
+    sub t (TAp a b) | Just t <- extractMetaVar t = do
hunk ./FrontEnd/Tc/Unify.hs 58
-
+-}
hunk ./FrontEnd/Tc/Unify.hs 66
-    sub s1@(TForAll as (_ :=> _))  r2 | isRho' r2 = do
+    sub s1@(TForAll as (_ :=> _))  r2  = do   -- isRho' r2
hunk ./FrontEnd/Tc/Unify.hs 85
-    sub t@(TArrow s1 s2) (TBox { typeBox = box}) = do
-        a <- newBox (kind s1)
-        b <- newBox (kind s2)
+    sub t@(TArrow s1 s2) (TMetaVar mv) = do
+        a <- newMetaVar (metaType mv) (kind s1)
+        b <- newMetaVar (metaType mv) (kind s2)
+        varBind mv (a `fn` b)
hunk ./FrontEnd/Tc/Unify.hs 90
-        fillBox box (a `fn` b)
+        --fillBox box (a `fn` b)
hunk ./FrontEnd/Tc/Unify.hs 93
-    sub a b | isTau a = case b of
-        (TBox {typeBox = b}) -> fillBox b a
-        _ | isTau b -> unify a b -- TODO verify? fail $ "taus don't match in MONO" ++ show (a,b)
-        _ -> do
-            fail $ "subsumes failure: "  <> ppretty s1 <+> ppretty s2
+    sub a b | isTau a && isTau b = unify a b
hunk ./FrontEnd/Tc/Unify.hs 100
-    s1 <- aquireType s1
-    s2 <- aquireType s2
+    s1 <- findType s1
+    s2 <- findType s2
hunk ./FrontEnd/Tc/Unify.hs 111
-    bm TBox { typeKind = k1, typeBox = ba} TBox { typeKind = k2, typeBox = bb} = do
-        when (k1 /= k2) $ error "boxyMatch kinds"
-        tt <- newTVar k1
-        fillBox ba tt
-        fillBox bb tt
+    bm (TMetaVar v1) (TMetaVar v2) = do
+        when (kind v1 /= kind v2) $ error "BBEQ boxyMatch kinds"
+        -- create a new metavar to enforce tauness.
+        tt <- newMetaVar Tau (kind v1)
+        varBind v1 tt
+        varBind v2 tt
hunk ./FrontEnd/Tc/Unify.hs 120
-    bm (TArrow s1 s2) TBox { typeBox = box} = do
+    bm (TArrow s1 s2) (TMetaVar mv) = do
hunk ./FrontEnd/Tc/Unify.hs 124
-        fillBox box (a `fn` b)
+        varBind mv (a `fn` b)
hunk ./FrontEnd/Tc/Unify.hs 135
-    bm a (TBox { typeBox = box }) | (TCon ca,as) <- fromTAp a = do
+    bm a (TMetaVar mv) | (TCon ca,as) <- fromTAp a = do
hunk ./FrontEnd/Tc/Unify.hs 138
-        fillBox box (foldl TAp (TCon ca) bs)
+        varBind mv (foldl TAp (TCon ca) bs)
hunk ./FrontEnd/Tc/Unify.hs 153
-    bm (TForAll vs (ps :=> t)) (TBox { typeKind = k, typeBox = box }) = do
-        a <- newBox k
+    bm (TForAll vs (ps :=> t)) (TMetaVar mv) = do
+        a <- newBox (kind mv)
hunk ./FrontEnd/Tc/Unify.hs 156
-        fillBox box (TForAll vs (ps :=> a))
+        varBind mv (TForAll vs (ps :=> a))
hunk ./FrontEnd/Tc/Unify.hs 169
-    bm (TArrow a b) t | Just t <- extractMetaTV t = do
+    -- XXX app
+    bm (TAp a b) (TAp c d) = do
+        a `boxyMatch` c
+        b `boxyMatch` d
+        return False
+
+    -- MEQ1 MEQ2  SYM
+    bm a b
+        | isTau a, TMetaVar mv <- b = varBind mv a >> return False
+        | isTau a && isTau b = unify a b >> return False
+
+{-
+    bm (TArrow a b) t | Just t <- extractMetaVar t = do
hunk ./FrontEnd/Tc/Unify.hs 187
-    bm (TAp a b) t | Just t <- extractMetaTV t = do
+    bm (TAp a b) t | Just t <- extractMetaVar t = do
hunk ./FrontEnd/Tc/Unify.hs 193
+  -}
hunk ./FrontEnd/Tc/Unify.hs 195
-    -- XXX app
-    bm (TAp a b) (TAp c d) = do
-        a `boxyMatch` c
-        b `boxyMatch` d
-        return False
-
-    -- MEQ1 MEQ2  SYM
-    bm a b | isTau a = case b of
-        (TBox { typeBox = b}) -> fillBox b a >> return False
-        _ | isTau b -> unify a b >> return False -- TODO, verify? fail $ "taus don't match in MEQ[12]" ++ show (a,b)
-          | otherwise -> return True
hunk ./FrontEnd/Tc/Unify.hs 202
+    liftIO $ putStrLn $ "unify: " <> ppretty t1 <+> ppretty t2
hunk ./FrontEnd/Tc/Unify.hs 213
-mgu (TVar u) t | isMetaTV u  = varBind u t
-mgu t (TVar u) | isMetaTV u  = varBind u t
+mgu (TMetaVar u) t = varBind u t
+mgu t (TMetaVar u) = varBind u t
hunk ./FrontEnd/Type.hs 26
-module Type (kind,
-             nullSubst,
+module Type (nullSubst,
hunk ./FrontEnd/Type.hs 40
+             HasKind(..),
hunk ./FrontEnd/Type.hs 101
+  kind (TMetaVar mv) = kind mv
hunk ./FrontEnd/Type.hs 103
+instance HasKind MetaVar where
+    kind = metaKind