[clean up tc code
John Meacham <john@repetae.net>**20051209060647] hunk ./FrontEnd/KindInfer.hs 11
+    hsQualTypeToSigma,
hunk ./FrontEnd/KindInfer.hs 37
-import Type(quantify,tv,tTTuple)
+import Type(quantify,tv,tTTuple,schemeToType)
hunk ./FrontEnd/KindInfer.hs 565
+hsQualTypeToSigma :: Monad m => KindEnv -> HsQualType -> m Sigma
+hsQualTypeToSigma kt qualType =  return $ schemeToType $ aHsQualTypeToScheme newEnv qualType where
+   newEnv = kiHsQualType kt qualType
hunk ./FrontEnd/Representation.hs 164
+            ft (TForAll vs qt) = do
+                qt' <- flattenType' qt
+                return $ TForAll vs qt'
+            ft (TBox _ box) = do
+                readIORef box
hunk ./FrontEnd/Tc/Main.hs 10
+import Control.Monad.Reader
hunk ./FrontEnd/Tc/Main.hs 16
-import FrontEnd.KindInfer(KindEnv)
+import FrontEnd.KindInfer(KindEnv,hsQualTypeToSigma)
+import FrontEnd.Tc.Monad
+import FrontEnd.Tc.Type
hunk ./FrontEnd/Tc/Main.hs 28
-import FrontEnd.Tc.Monad
-import FrontEnd.Tc.Type
-
hunk ./FrontEnd/Tc/Main.hs 46
-addPreds :: [Pred] -> Tc ()
-addPreds = tell
hunk ./FrontEnd/Tc/Main.hs 50
-    t <- br
-    e2 <- tiExpr e2 t  -- TODO Poly
+    t <- br >>= findType
+    e2 <- tiExprPoly e2 t  -- TODO Poly
hunk ./FrontEnd/Tc/Main.hs 54
+tiExprPoly ::  HsExp -> Type ->  Tc HsExp
+
+tiExprPoly e t@TBox {} = tiExpr e t
+tiExprPoly e t = do
+    t' <- freshInstance t
+    tiExpr e t'
+
hunk ./FrontEnd/Tc/Main.hs 66
-    (ps :=> t) <- freshInst sc
-    addPreds ps
-    t `subsumes` typ
+    sc <- freshInstance sc
+    sc `subsumes` typ
hunk ./FrontEnd/Tc/Main.hs 72
-    ((ps :=> t)) <- freshInst sc
-    addPreds ps
-    t `subsumes` typ
+    sc <- freshInstance sc
+    sc `subsumes` typ
hunk ./FrontEnd/Tc/Main.hs 86
---tiExpr (HsExpTypeSig sloc e qt) typ =  withContext (locMsg sloc "in the annotated expression" $ render $ ppHsExp expr) $ do
+-- comb LET-S and VAR
+tiExpr expr@(HsExpTypeSig sloc e qt) typ =  withContext (locMsg sloc "in the annotated expression" $ render $ ppHsExp expr) $ do
+    kt <- getKindEnv
+    s <- hsQualTypeToSigma kt qt
+    r <- freshInstance s
+    e' <- tiExpr e r
+    s' <- freshSigma s
+    s' `subsumes` typ
+    return (HsExpTypeSig sloc e' qt)
+
hunk ./FrontEnd/Tc/Main.hs 120
-            (_,b1) <- newBox Star
-            (_,b2) <- newBox Star
-            lam (p:ps) e (b1 `fn` b2) rs
+            (rs1,b1) <- newBox Star
+            (rs2,b2) <- newBox Star
+            r <- lam (p:ps) e (b1 `fn` b2) rs
+            s1 <- rs1 >>= findType
+            s2 <- rs2 >>= findType
+            fillBox box (s1 `fn` s2)
+            return r
hunk ./FrontEnd/Tc/Main.hs 130
-            s1 <- br
+            s1 <- br >>= findType
hunk ./FrontEnd/Tc/Main.hs 133
-                lam ps e s2' (p':rs)  -- TODO poly
+                lamPoly ps e s2' (p':rs)  -- TODO poly
hunk ./FrontEnd/Tc/Main.hs 138
+        lamPoly ps e s@TBox {} rs = lam ps e s rs
+        lamPoly ps e s rs = do
+            s <- freshInstance s
+            lam ps e s rs
+
+
hunk ./FrontEnd/Tc/Main.hs 181
---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 expr@(HsLet [HsPatBind sl (HsPVar x) (HsUnGuardedRhs u) []] t) typ = withContext (makeMsg "in the let binding" $ render $ ppHsExp expr) $ do
+    (rb,tb) <- newBox Star
+    u' <- tiExpr u tb
+    rr <- rb >>= findType
+    rr <- generalize rr
+    t' <- localEnv (Map.singleton (toName Val x) rr) $ do
+        tiExpr t typ
+    return (HsLet [HsPatBind sl (HsPVar x) (HsUnGuardedRhs u') []] t')
hunk ./FrontEnd/Tc/Monad.hs 2
-    TypeEnv(),
-    Tc(),
-    localEnv,
+    addPreds,
hunk ./FrontEnd/Tc/Monad.hs 4
-    tcInfoEmpty,
-    runTc,
+    freshInstance,
+    freshSigma,
+    getKindEnv,
+    inst,
+    localEnv,
hunk ./FrontEnd/Tc/Monad.hs 10
-    freshInst,
-    unify,
-    newTVar,
hunk ./FrontEnd/Tc/Monad.hs 11
-    withContext,
-    inst,
+    newTVar,
+    runTc,
+    Tc(),
+    TcInfo(..),
+    tcInfoEmpty,
+    TypeEnv(),
+    unify,
hunk ./FrontEnd/Tc/Monad.hs 19
-    TcInfo(..)
+    generalize,
+    withContext
hunk ./FrontEnd/Tc/Monad.hs 39
-import Type(mgu)
+import Type(mgu,tv)
hunk ./FrontEnd/Tc/Monad.hs 261
+freshInstance :: Sigma -> Tc Rho
+freshInstance (TForAll as qt) = do
+    ts <- mapM newTVar (map tyvarKind as)
+    let (ps :=> t) = (inst (Map.fromList $ zip (map tyvarAtom as) ts) qt)
+    addPreds ps
+    return t
+freshInstance x = return x
+
+addPreds :: [Pred] -> Tc ()
+addPreds = tell
+
+newVar :: Kind -> Tc Tyvar
+newVar k = do
+    te <- ask
+    n <- newUniq
+    let ident = toName TypeVal (tcInfoModName $ tcInfo te,'v':show n)
+        v = tyvar ident k Nothing
+    return v
+
+-- rename the bound variables of a sigma, just in case.
+freshSigma :: Sigma -> Tc Sigma
+freshSigma (TForAll [] ([] :=> t)) = return t
+freshSigma (TForAll vs qt) = do
+    nvs <- mapM (newVar . tyvarKind) vs
+    return (TForAll nvs $ inst (Map.fromList $ zip (map tyvarAtom vs) (map TVar nvs)) qt)
+freshSigma x = return x
+
+-- | replace bound variables with arbitrary new ones and drop the binding
+-- TODO predicates?
+
+skolomize :: Type -> Tc ([Tyvar],Type)
+skolomize s = freshSigma s >>= \x -> case x of
+    TForAll as (_ :=> r) -> return (as,r)
hunk ./FrontEnd/Tc/Monad.hs 296
+boxyInstantiate :: Sigma -> Tc Rho
+boxyInstantiate (TForAll as (ps :=> r)) = do
+
+
+
+--    sub (TForAll as (_ :=> r1))  r2 | isRho' r2 = do
+        bs <- mapM (const $ newBox Star) as
+        inst (Map.fromList $ zip (map tyvarAtom as) (snds bs)) r1 `subsumes` r2
+  -}
+{-
+newSigma :: Sigma -> Tc ([Tyvar],Rho)
+newSigma (TForAll vs qt) = do
+    nvs <- mapM (newVar . tyvarKind) vs
+    return (nvs,inst (Map.fromList $ zip (map tyvarAtom vs) (map TVar nvs)) qt)
+newSigma x = return ([],x)
+
hunk ./FrontEnd/Tc/Monad.hs 319
+generalize :: Rho -> Tc Sigma
+generalize r = do
+    freshSigma (TForAll (tv r) ([] :=> r))
hunk ./FrontEnd/Tc/Type.hs 17
+type MetaTV = Tyvar
+type SkolemTV = Tyvar
+type BoundTV = Tyvar
+
hunk ./FrontEnd/Tc/Type.hs 46
--- SBOXY
-subsumes (TBox k a) b = boxyMatch (TBox k a) b
+subsumes s1 s2 = do
+    s1 <- findType s1
+    s2 <- findType s2
+    sub s1 s2
+   where
+    -- SBOXY
+    sub (TBox k a) b = boxyMatch (TBox k a) b
+
+    -- SKOL needs to be after SBOXY
+    sub s1 fa@TForAll {} = do
+        r1 <- freshInstance fa
+        s1 `subsumes` r1
hunk ./FrontEnd/Tc/Type.hs 59
--- SKOL needs to be after SBOXY
-subsumes s1 fa@TForAll {} = do
-    ps :=> r1 <- freshInst fa
-    tell ps
-    s1 `subsumes` r1
+    -- SPEC
+    sub (TForAll as (_ :=> r1))  r2 | isRho' r2 = do
+        bs <- mapM (const $ newBox Star) as
+        inst (Map.fromList $ zip (map tyvarAtom as) (snds bs)) r1 `subsumes` r2
hunk ./FrontEnd/Tc/Type.hs 64
--- SPEC
-subsumes (TForAll as (_ :=> r1))  r2 | isRho' r2 = do
-    bs <- mapM (const $ newBox Star) as
-    inst (Map.fromList $ zip (map tyvarAtom as) (snds bs)) r1 `subsumes` r2
+    -- CON (??)
+    sub s1@TAp {} s2 = s1 `boxyMatch` s2
hunk ./FrontEnd/Tc/Type.hs 67
--- CON (??)
-subsumes s1@TAp {} s2 = s1 `boxyMatch` s2
+    -- F1
+    sub (TArrow s1 s2) (TArrow s3 s4) = do
+        boxyMatch s3 s1
+        subsumes s2 s4
+    -- F2
+    sub t@(TArrow _ _) (TBox _ box) = do
+        (oa,a) <- newBox Star
+        (ob,b) <- newBox Star
+        subsumes t (a `fn` b)
+        na <- oa
+        nb <- ob
+        fillBox box (na `fn` nb)
hunk ./FrontEnd/Tc/Type.hs 80
--- F1
-subsumes (TArrow s1 s2) (TArrow s3 s4) = do
-    boxyMatch s3 s1
-    subsumes s2 s4
--- F2
-subsumes t@(TArrow _ _) (TBox _ box) = do
-    (oa,a) <- newBox Star
-    (ob,b) <- newBox Star
-    subsumes t (a `fn` b)
-    na <- oa
-    nb <- ob
-    fillBox box (na `fn` nb)
+    -- BMONO & MONO
+    sub a b | isTau a = case b of
+        (TBox _ b) -> fillBox b a
+        _ | isTau b -> unify a b -- TODO verify? fail $ "taus don't match in MONO" ++ show (a,b)
+        _ -> fail $ "subsumes: " ++ show (a,b)
hunk ./FrontEnd/Tc/Type.hs 86
--- BMONO & MONO
-subsumes a b | isTau a = case b of
-    (TBox _ b) -> fillBox b a
-    _ | isTau b -> unify a b -- TODO verify? fail $ "taus don't match in MONO" ++ show (a,b)
---    _ | a == b -> return ()
+    sub a b = fail $ "subsumes: " ++ show (a,b)
hunk ./FrontEnd/Tc/Type.hs 88
--- -- MONO
--- subsumes (TCon a) (TCon b) | a == b = return ()
hunk ./FrontEnd/Tc/Type.hs 90
+boxyMatch s1 s2 = do
+    s1 <- findType s1
+    s2 <- findType s2
+    b <- bm s1 s2
+    if b then do
+        b' <- bm s2 s1
+        when b' $  fail $ "boxyMatch failure: " ++ show (s1,s2)
+     else return ()
+   where
+    -- BBEQ
+    bm (TBox k1 ba) (TBox k2 bb) = do
+        when (k1 /= k2) $ error "boxyMatch kinds"
+        tt <- newTVar k1
+        fillBox ba tt
+        fillBox bb tt
+        return False
+
+    -- AEQ1
+    bm (TArrow s1 s2) (TBox _ box) = do
+        (ra,a) <- newBox Star
+        (rb,b) <- newBox Star
+        boxyMatch (s1 `fn` s2) (a `fn` b)
+        x <- ra
+        y <- rb
+        fillBox box (x `fn` y)
+        return False
+
+    -- AEQ2
+    bm (TArrow s1 s2) (TArrow s3 s4) = do
+        boxyMatch s1 s3
+        boxyMatch s2 s4
+        return False
+
+    -- CEQ1
+
+    bm a (TBox _ box) | (TCon ca,as) <- fromTAp a = do
+        bs <- mapM (const $ newBox Star) as
+        sequence_ [boxyMatch x y | x <- as | y <- snds bs]
+        bs <- sequence $ fsts bs
+        fillBox box (foldl TAp (TCon ca) bs)
+        return False
+
+
+    -- CEQ2
+
+    bm a b | (TCon ca,as) <- fromTAp a, (TCon cb,bs) <- fromTAp b = case ca == cb of
+        False -> fail $ "constructor mismatch: " ++ show (a,b)
+        True -> sequence_ [boxyMatch x y | x <- as | y <- bs] >> return False
+
+
+    -- SEQ1
+    bm (TForAll vs (ps :=> t)) (TBox _ box) = do
+        (ra,a) <- newBox Star
+        boxyMatch t a
+        a <- ra
+        fillBox box (TForAll vs (ps :=> a))
+        return False
hunk ./FrontEnd/Tc/Type.hs 148
--- BBEQ
-boxyMatch (TBox k1 ba) (TBox k2 bb) = do
-    when (k1 /= k2) $ error "boxyMatch kinds"
-    tt <- newTVar k1 -- is star always right?
-    fillBox ba tt
-    fillBox bb tt
+    -- SEQ2
hunk ./FrontEnd/Tc/Type.hs 150
--- AEQ1
-boxyMatch (TArrow s1 s2) (TBox _ box) = do
-    (ra,a) <- newBox Star
-    (rb,b) <- newBox Star
-    boxyMatch (s1 `fn` s2) (a `fn` b)
-    x <- ra
-    y <- rb
-    fillBox box (x `fn` y)
+    bm (TForAll vs (ps :=> t)) (TForAll vs' (ps' :=> t')) = fail "SEQ2"
+    -- >> do
+    --    (ra,a) <- newBox Star
+    --    boxyMatch t a
+    --    a <- ra
+     --   fillBox box (TForAll vs (ps :=> a))
+     --   return False
hunk ./FrontEnd/Tc/Type.hs 158
--- AEQ2
-boxyMatch (TArrow s1 s2) (TArrow s3 s4) = do
-    boxyMatch s1 s3
-    boxyMatch s2 s4
hunk ./FrontEnd/Tc/Type.hs 159
--- SEQ1
---boxyMatch
+    -- MEQ1 MEQ2  SYM
+    bm a b | isTau a = case b of
+        (TBox _ 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
+    bm _ _ = return True
hunk ./FrontEnd/Tc/Type.hs 166
--- MEQ1 MEQ2
-boxyMatch a b | isTau a = case b of
-    (TBox _ b) -> fillBox b a
-    _ | isTau b -> unify a b -- TODO, verify? fail $ "taus don't match in MEQ[12]" ++ show (a,b)
---    _ | a == b -> return ()
hunk ./FrontEnd/Tc/Type.hs 167
--- SYM (careful!)
-boxyMatch a b = boxyMatch b a
+fromTAp t = f t [] where
+    f (TAp a b) rs = f a (b:rs)
+    f t rs = (t,reverse rs)
hunk ./FrontEnd/Type.hs 100
+  kind (TBox k _) = k
hunk ./Interactive.hs 181
+    when False $ do
hunk ./Interactive.hs 218
+    ps' <- flattenType ps'