[start using boxy matching primitives, enforce tau rules.
John Meacham <john@repetae.net>**20051208101702] hunk ./FrontEnd/KindInfer.hs 557
-   = IsIn (toName ClassName className) (TVar $ tyvar (toName TypeVal varName) (head $ kindOfClass (toName ClassName className) kt) Nothing)
+   | isConstructorLike (hsIdentString . hsNameIdent $ varName) = IsIn  (toName ClassName className) (TCon (Tycon (toName TypeConstructor varName) (head $ kindOfClass (toName ClassName className) kt)))
+   | otherwise = IsIn (toName ClassName className) (TVar $ tyvar (toName TypeVal varName) (head $ kindOfClass (toName ClassName className) kt) Nothing)
hunk ./FrontEnd/Representation.hs 71
-           | TBox { typeBox :: IORef Type }     -- ^ used only in typechecker
+           | TBox { typeKind :: Kind, typeBox :: IORef Type }     -- ^ used only in typechecker
hunk ./FrontEnd/Representation.hs 249
+           TBox Star _ -> text "_"
+           TBox k _ -> return $ parens $ text "_ :: " <> pprint k
hunk ./FrontEnd/Tc/Main.hs 49
+tcApp e1 e2 typ = do
+    (br,bt) <- newBox Star
+    e1 <- tiExpr e1 (bt `fn` typ)
+    t <- br
+    e2 <- tiExpr e2 t  -- TODO Poly
+    return (e1,e2)
+
hunk ./FrontEnd/Tc/Main.hs 63
-    unify t typ
+    t `subsumes` typ
hunk ./FrontEnd/Tc/Main.hs 69
-    unify t typ
hunk ./FrontEnd/Tc/Main.hs 70
+    t `subsumes` typ
hunk ./FrontEnd/Tc/Main.hs 75
-    unify t typ
+    t `subsumes` typ
hunk ./FrontEnd/Tc/Main.hs 83
+
hunk ./FrontEnd/Tc/Main.hs 85
-    (br,bt) <- newBox
-    e1 <- tiExpr e1 (bt `TArrow` typ)
-    t <- br
-    e2 <- tiExpr e2 t
+    (e1,e2) <- tcApp e1 e2 typ
hunk ./FrontEnd/Tc/Main.hs 88
+tiExpr expr@(HsInfixApp e1 e2 e3) typ = withContext (makeMsg "in the infix application" $ render $ ppHsExp expr) $ do
+    (HsApp e2 e1,e3) <- tcApp (HsApp e2 e1) e3 typ   -- TODO, preserve
+    return (HsInfixApp e1 e2 e3)
hunk ./FrontEnd/Tc/Main.hs 92
-
hunk ./FrontEnd/Tc/Main.hs 101
-{-
-tiExpr expr@(HsLambda sloc pats e) typ = withContext (locSimple sloc $ "in the lambda expression\n   \\" ++ show pats ++ " -> ...") $ do
-        ts <- mapM (const newBox) pats
-        (ps, envP) <- tiPats pats ts
-        (br,bt) <- newBox
-        qs <- localEnv envP $ do
-            tiExpr e bt
-        t <- br
-        unify (foldr fn t ts) typ
-        return (ps ++ qs)
-        --(ps, envP, ts) <- tiPats pats
-        --(qs, envE, t)  <- tiExpr (envP `Map.union` env) e
hunk ./FrontEnd/Tc/Main.hs 102
-        --return (ps++qs, envP `Map.union` envE, foldr fn t ts)  -- Boba
--}
+-- ABS1
+tiExpr expr@(HsLambda sloc ps e) typ = withContext (locSimple sloc $ "in the lambda expression\n   \\" ++ show ps ++ " -> ...") $ do
+    let lam (p:ps) e (TBox _ box) rs = do -- ABS2
+            (_,b1) <- newBox Star
+            (_,b2) <- newBox Star
+            lam (p:ps) e (b1 `fn` b2) rs
+        lam (p:ps) e (TArrow s1' s2') rs = do -- ABS1
+            (br,box) <- newBox Star
+            s1' `boxyMatch` box
+            s1 <- br
+            (p',env) <- tiPat p s1
+            localEnv env $ do
+                lam ps e s2' (p':rs)  -- TODO poly
+        lam [] e typ rs = do
+            e' <- tiExpr e typ
+            return (HsLambda sloc (reverse rs) e')
+        lam _ _ _ _ = fail "lambda type mismatch"
+    lam ps e typ []
+
+
hunk ./FrontEnd/Tc/Main.hs 128
+-- tuples can't be empty, () is not a tuple
+--tiExpr env tuple@(HsTuple exps@(_:_)) typ = withContext (makeMsg "in the tuple" $ render $ ppHsExp tuple) $ do
+--    psasts <- mapM tiExpr exps
+--    let typeList = map trd3 psasts
+--    let preds = concatMap fst3 psasts
+--    let env1 = Map.unions $ map snd3 psasts
+--    return (preds, env1, tTTuple typeList)
hunk ./FrontEnd/Tc/Main.hs 136
+-- special case for the empty list
+tiExpr (HsList []) typ = do
+        v <- newTVar Star
+        (TAp tList v) `subsumes` typ
+        return (HsList [])
+
+-- non empty list
+tiExpr expr@(HsList exps@(_:_)) typ = withContext (makeMsg "in the list " $ render $ ppHsExp expr) $ do
+        v <- newTVar Star
+        exps' <- mapM (`tiExpr` v) exps
+        (TAp tList v) `subsumes` typ
+        return (HsList exps')
+
hunk ./FrontEnd/Tc/Main.hs 156
-tiExpr e typ = error $ "tiExpr: not implemented for: " ++ show (e,typ)
+--tiExpr env expr@(HsLet decls e) = withContext (makeMsg "in the let binding" $ render $ ppHsExp expr) $ do
+--         sigEnv <- getSigEnv
+--         let bgs = getFunDeclsBg sigEnv decls
+--         (ps, env1) <- tiSeq tiBindGroup env bgs
+--         (qs, env2, t) <- tiExpr (env1 `Map.union` env) e
+--         -- keep the let bound type assumptions in the environment
+
+tiExpr e typ = fail $ "tiExpr: not implemented for: " ++ show (e,typ)
hunk ./FrontEnd/Tc/Main.hs 168
-tiPat :: HsPat -> Type -> Tc (HsPat, Map.Map Name Scheme)
+tiPat :: HsPat -> Type -> Tc (HsPat, Map.Map Name Sigma)
hunk ./FrontEnd/Tc/Main.hs 172
-        unify v typ
-        --let newAssump = assumpToPair $ makeAssump i (toScheme v)
-        --let newAssump = (i,toScheme v)
-        return (HsPVar i, Map.singleton (toName Val i) (toScheme v))
+        v `subsumes` typ
+        return (HsPVar i, Map.singleton (toName Val i) v)
hunk ./FrontEnd/Tc/Main.hs 177
-    unify t typ
+    t `subsumes` typ
hunk ./FrontEnd/Tc/Monad.hs 172
-newBox :: Tc (Tc Type,Type)
-newBox = do
+newBox :: Kind -> Tc (Tc Type,Type)
+newBox k = do
hunk ./FrontEnd/Tc/Monad.hs 175
-    return (liftIO $ readIORef r, TBox r)
+    return (liftIO $ readIORef r, TBox k r)
hunk ./FrontEnd/Tc/Monad.hs 282
-        liftIO $ typeError (Failure s) (tcDiagnostics st)
+        liftIO $ fail s -- typeError (Failure s) (tcDiagnostics st)
hunk ./FrontEnd/Tc/Type.hs 13
-type BoxySigma = Sigma
+type Sigma' = Sigma
+type Tau' = Tau
+type Rho' = Rho
hunk ./FrontEnd/Tc/Type.hs 41
-subsumes :: BoxySigma -> BoxySigma -> Tc ()
+subsumes :: Sigma' -> Sigma' -> Tc ()
hunk ./FrontEnd/Tc/Type.hs 43
-subsumes (TBox a) b = boxyMatch (TBox a) b
+subsumes (TBox k a) b = boxyMatch (TBox k a) b
hunk ./FrontEnd/Tc/Type.hs 53
-    bs <- mapM (const newBox) as
+    bs <- mapM (const $ newBox Star) as
hunk ./FrontEnd/Tc/Type.hs 64
-subsumes t@(TArrow _ _) (TBox box) = do
-    (oa,a) <- newBox
-    (ob,b) <- newBox
+subsumes t@(TArrow _ _) (TBox _ box) = do
+    (oa,a) <- newBox Star
+    (ob,b) <- newBox Star
hunk ./FrontEnd/Tc/Type.hs 74
-    (TBox b) -> fillBox b a
-    _ | a == b -> return ()
+    (TBox _ b) -> fillBox b a
+--    _ | a == b -> return ()
hunk ./FrontEnd/Tc/Type.hs 81
-boxyMatch :: BoxySigma -> BoxySigma -> Tc ()
+boxyMatch :: Sigma' -> Sigma' -> Tc ()
hunk ./FrontEnd/Tc/Type.hs 84
-boxyMatch (TBox ba) (TBox bb) = do
-    tt <- newTVar Star -- is star always right?
+boxyMatch (TBox k1 ba) (TBox k2 bb) = do
+    when (k1 /= k2) $ error "boxyMatch kinds"
+    tt <- newTVar k1 -- is star always right?
hunk ./FrontEnd/Tc/Type.hs 91
-boxyMatch (TArrow s1 s2) (TBox box) = do
-    (ra,a) <- newBox
-    (rb,b) <- newBox
+boxyMatch (TArrow s1 s2) (TBox _ box) = do
+    (ra,a) <- newBox Star
+    (rb,b) <- newBox Star
hunk ./FrontEnd/Tc/Type.hs 109
-    (TBox b) -> fillBox b a
-    _ | a == b -> return ()
+    (TBox _ b) -> fillBox b a
+--    _ | a == b -> return ()
hunk ./FrontEnd/Type.hs 177
--- boxes on the right are always empty, boxes on the left are full (for now)
hunk ./FrontEnd/Type.hs 178
-mgu' t (TBox box) = do
-    liftIO $ writeIORef box t
-    return nullSubst
+--mgu' t (TBox box) = do
+--    liftIO $ writeIORef box t
+--    return nullSubst
hunk ./FrontEnd/Type.hs 202
-mgu' (TBox box) t2 = do
-    t1 <- liftIO $ readIORef box
-    mgu'' t1 t2
-    return nullSubst
+--mgu' (TBox box) t2 = do
+--    t1 <- liftIO $ readIORef box
+--    mgu'' t1 t2
+--    return nullSubst
hunk ./Interactive.hs 215
-    (rbox,box) <- newBox
+    (rbox,box) <- newBox Star