[more work on new typechecker
John Meacham <john@repetae.net>**20060212114652] hunk ./FrontEnd/Representation.hs 73
-           | TBox { typeKind :: Kind, typeSeq :: !Int, typeBox :: IORef (Maybe Type) }     -- ^ used only in typechecker
hunk ./FrontEnd/Representation.hs 175
-            --ft (TBox _ _ box) = do
-            --    readIORef box
-            ft TBox {} = error "odd box"
hunk ./FrontEnd/Representation.hs 260
-           TBox Star i _ -> text "_" <> tshow i
-           TBox k i _ -> return $ parens $ text "_" <> tshow i <> text " :: " <> pprint k
hunk ./FrontEnd/Tc/Main.hs 63
-    (_,False,_) <- unbox t
+    --(_,False,_) <- unbox t
hunk ./FrontEnd/Tc/Main.hs 151
-            b1 <- newBox Star
-            b2 <- newBox Star
-            varBind mv (b1 `fn` b2)
-            l' <- lam (p:ps) e (b1 `fn` b2) rs
+            withMetaVars mv [Star,Star] (\ [a,b] -> a `fn` b) $ \ [a,b] -> lam (p:ps) e (a `fn` b) rs
+            --b1 <- newBox Star
+            --b2 <- newBox Star
+            --varBind mv (b1 `fn` b2)
+            --l' <- lam (p:ps) e (b1 `fn` b2) rs
hunk ./FrontEnd/Tc/Main.hs 157
-            return l'
+            --return l'
hunk ./FrontEnd/Tc/Main.hs 188
+-- special case for the empty list
+tiExpr (HsList []) (TAp c v) | c == tList = do
+    unBox v
+    return (HsList [])
+
hunk ./FrontEnd/Tc/Main.hs 195
-        v <- newBox Star
-        (TAp tList v) `subsumes` typ
-        return (HsList [])
+    v <- newVar Star
+    let lt = TForAll [v] ([] :=> TAp tList (TVar v))
+    lt `subsumes` typ
+    return (HsList [])
+
+-- non empty list
+tiExpr expr@(HsList exps@(_:_)) (TAp tList' v) | tList == tList' = withContext (makeMsg "in the list " $ render $ ppHsExp expr) $ do
+        exps' <- mapM (`tcExpr` v) exps
+        return (HsList exps')
hunk ./FrontEnd/Tc/Main.hs 207
-        --v <- newTVar Star
hunk ./FrontEnd/Tc/Main.hs 291
-        v <- newBox Star
+        --v <- newMetaVar Tau Star
hunk ./FrontEnd/Tc/Main.hs 293
-        typ `subsumes` v
-        addToCollectedEnv (Map.singleton (toName Val i) v)
-        return (HsPVar i, Map.singleton (toName Val i) v)
+        --typ `subsumes` v
+        typ' <- unBox typ
+        addToCollectedEnv (Map.singleton (toName Val i) typ')
+        return (HsPVar i, Map.singleton (toName Val i) typ')
hunk ./FrontEnd/Tc/Main.hs 318
-    --s `boxyMatch` (foldr fn typ bs)
hunk ./FrontEnd/Tc/Main.hs 319
-    --(foldr fn typ bs) `subsumes` s
hunk ./FrontEnd/Tc/Main.hs 324
-    --typ `subsumes` TAp tList v
-    --v `subsumes` TAp tList v
-    v' <- newBox Star
-    v `subsumes` v'
+    unBox v
hunk ./FrontEnd/Tc/Main.hs 329
-    typ `subsumes` TAp tList v
+    --typ `subsumes` TAp tList v
+    typ `boxyMatch` TAp tList v
hunk ./FrontEnd/Tc/Main.hs 343
-    typ `subsumes` TAp tList v
hunk ./FrontEnd/Tc/Main.hs 344
+    typ `boxyMatch` TAp tList v
hunk ./FrontEnd/Tc/Main.hs 347
-tiPat HsPWildCard typ = return (HsPWildCard, mempty)
+tiPat HsPWildCard typ = unBox typ >> return (HsPWildCard, mempty)
hunk ./FrontEnd/Tc/Monad.hs 16
+    withMetaVars,
hunk ./FrontEnd/Tc/Monad.hs 20
+    unBox,
hunk ./FrontEnd/Tc/Monad.hs 22
-    newTVar,
hunk ./FrontEnd/Tc/Monad.hs 191
-newTVar :: Kind -> Tc Type
-newTVar k = newMetaVar Sigma k
-
hunk ./FrontEnd/Tc/Monad.hs 262
-skolomize s@TForAll {} = freshSigma s >>= \x -> case x of
-    TForAll as (_ :=> r) -> return (as,r)
-    r -> return ([],r)
+skolomize (TForAll vs (_ :=> rho)) = return (vs,rho) 
+--freshSigma s >>= \x -> case x of
+--    TForAll as (_ :=> r) -> return (as,r)
+--    r -> return ([],r)
hunk ./FrontEnd/Tc/Monad.hs 418
+withMetaVars :: MetaVar -> [Kind] -> ([Sigma] -> Sigma) -> ([Sigma'] -> Tc a) -> Tc a
+withMetaVars mv ks sfunc bsfunc | isBoxyMetaVar mv = do
+    boxes <- mapM newBox ks
+    res <- bsfunc boxes
+    tys <- mapM readFilledBox [ mv | ~(TMetaVar mv) <- boxes]
+    varBind mv (sfunc tys)
+    return res
+withMetaVars mv ks sfunc bsfunc  = do
+    taus <- mapM (newMetaVar Tau) ks
+    varBind mv (sfunc taus)
+    bsfunc taus
+    
hunk ./FrontEnd/Tc/Unify.hs 9
+import Support.CanType
hunk ./FrontEnd/Tc/Unify.hs 36
-        --r1 <- freshInstance fa
hunk ./FrontEnd/Tc/Unify.hs 47
+   -- sub s1 (TMetaVar mv) | (t,ts@(_:_)) <- fromTAp s1 = do
+   --     let ats = t:ts
+   --     withMetaVars mv (map getaType ats) (map  (\ (t:ts) -> TArrow a b) $ \ [a,b] -> do
+   --     subsumes t (a `fn` b)
+
+
hunk ./FrontEnd/Tc/Unify.hs 58
-    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
-        --fillBox box (a `fn` b)
+    sub t@(TArrow s1 s2) (TMetaVar mv) = do
+        withMetaVars mv [getType s1, getType s2] (\ [a,b] -> TArrow a b) $ \ [a,b] -> do
+        subsumes t (a `fn` b)
hunk ./FrontEnd/Tc/Unify.hs 90
-    bm (TMetaVar v1) (TMetaVar v2) | v1 == v2 = return False
-    -- BBEQ
hunk ./FrontEnd/Tc/Unify.hs 91
-        printRule "BBEQ"
-        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
+        var_meets_var v1 v2
hunk ./FrontEnd/Tc/Unify.hs 97
-        a <- newMetaVar Tau (kind s1)
-        b <- newMetaVar Tau (kind s2)
-        boxyMatch (s1 `fn` s2) (a `fn` b)
-        varBind mv (a `fn` b)
+        withMetaVars mv [getType s1, getType s2] (\ [t1,t2] -> TArrow t1 t2) $ \ [t1,t2] ->
+            boxyMatch s1 t1 >> boxyMatch s2 t2
hunk ./FrontEnd/Tc/Unify.hs 112
-    --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
+    bm a (TMetaVar mv) | (TCon ca,as) <- fromTAp a = do
+        withMetaVars mv (map getType as) (\ ts -> foldl TAp (TCon ca) ts) $ \ ts ->
+            sequence_ [ boxyMatch a t | t <- ts | a <- as ]
+        return False
+
+    bm a (TMetaVar mv) | (x,xs@(_:_)) <- fromTAp a = do
+        let xxs = x:xs
+        withMetaVars mv (map getType xxs) (\ (t:ts) -> foldl TAp t ts) $ \ ts ->
+            sequence_ [ boxyMatch a t | t <- ts | a <- xxs ]
+        return False
hunk ./FrontEnd/Tc/Unify.hs 139
-    bm (TForAll vs (ps :=> t)) (TMetaVar mv) = do
-        printRule "SEQ1"
-        a <- newBox (kind mv)
-        boxyMatch t a
-        varBind mv (TForAll vs (ps :=> a))
+    bm (TForAll vs (ps :=> tbody)) (TMetaVar mv) = do
+        withMetaVars mv [getType mv] (\ [t] -> TForAll vs (ps :=> t))  $ \ [t] ->
+            boxyMatch tbody t
hunk ./FrontEnd/Tc/Unify.hs 147
-    -- >> do
-    --    (ra,a) <- newBox Star
-    --    boxyMatch t a
-    --    a <- ra
-     --   fillBox box (TForAll vs (ps :=> a))
+    --bm a (TMetaVar mv)  = do
+     --   varBind mv a
hunk ./FrontEnd/Tc/Unify.hs 150
-    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 152
-    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
-{-
-    -- 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 164
-        -}
hunk ./FrontEnd/Tc/Unify.hs 169
+    bm _ _ = return True
hunk ./FrontEnd/Tc/Unify.hs 171
-{-
-    bm (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) `boxyMatch` (TArrow a' b')
-        return False
-    bm (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) `boxyMatch` (TAp a' b')
-        return False
-  -}
+var_meets_var :: MetaVar -> MetaVar -> Tc ()
+var_meets_var tv1 tv2 = do
+    when (getType tv1 /= getType tv2) $ error "BBEQ boxyMatch kinds"
+    f tv1 tv2
+    where
+    f tv1 tv2 | tv1 == tv2 = return ()
+    f tv1 tv2 | isBoxyMetaVar tv1 && isBoxyMetaVar tv2 = do
+            printRule "BBEQ"
+            tt <- newMetaVar Tau (kind tv1)
+            varBind tv1 tt
+            varBind tv2 tt
+    f tv1 tv2 | isBoxyMetaVar tv1  = do
+            printRule "BBEQ-L"
+            varBind tv1 (TMetaVar tv2)
+    f tv1 tv2 | isBoxyMetaVar tv2  = do
+            printRule "BBEQ-R"
+            varBind tv2 (TMetaVar tv1)
+    f tv1 tv2  = do
+            printRule "BBEQ-Tau"
+            varBind tv2 (TMetaVar tv1)
hunk ./FrontEnd/Tc/Unify.hs 192
-    bm _ _ = return True
hunk ./FrontEnd/Tc/Unify.hs 218
-mgu _ TBox {} = error "attempt to unify TBox"
-mgu TBox {} _ = error "attempt to unify TBox"
hunk ./FrontEnd/Tc/Unify.hs 224
+
+-- This is used in pattern matching because it might be polymorphic, but also needs to match exactly
+--subsumesPattern a b | isTau b = a `boxyMatch` b
+--subsumes
+
+
+
+
+
hunk ./FrontEnd/Type.hs 100
-  kind (TBox { typeKind = k }) = k
hunk ./FrontEnd/Type.hs 181
---mgu' t (TBox box) = do
---    liftIO $ writeIORef box t
---    return nullSubst
hunk ./FrontEnd/Type.hs 199
---mgu (TGen n tv) (TGen n' tv') | n == n' = varBind tv' (TVar tv)
hunk ./FrontEnd/Type.hs 201
---mgu' (TBox box) t2 = do
---    t1 <- liftIO $ readIORef box
---    mgu'' t1 t2
---    return nullSubst