[use coercions generated by typechecker rather than specialization to apply type variables
John Meacham <john@repetae.net>**20060302050431] hunk ./E/Eta.hs 1
-module E.Eta(etaExpand,etaExpandE) where
+module E.Eta(etaExpand,etaExpandE,etaReduce) where
hunk ./E/Eta.hs 75
+etaReduce :: E -> E
+etaReduce e = f e where
+        f (ELam t (EAp x (EVar t'))) | t == t' && not (tvrNum t `Set.member` freeVars x) = f x
+        f e = e
hunk ./E/Eta.hs 81
-etaReduce :: E -> (E,Int)
-etaReduce e = case f e 0 of
+etaReduce' :: E -> (E,Int)
+etaReduce' e = case f e 0 of
hunk ./E/FromHs.hs 33
+import E.Eta
hunk ./E/FromHs.hs 101
-    cvar _ Tyvar { tyvarRef = Just {}, tyvarKind = k}= error "tyvar is metaref"
+    cvar _ Tyvar { tyvarRef = Just {}, tyvarKind = k}= error $ "tyvar is metaref:" ++ prettyPrintType t
hunk ./E/FromHs.hs 150
+lookupCoercion n = do
+    assumps <- asks ceAssumps
+    cs <- asks ceCoerce
+    case Map.lookup n assumps of
+        Just x -> return (Left x)
+        Nothing -> Right `liftM` Map.lookup n cs
+
+
hunk ./E/FromHs.hs 308
-            cs <- flip mapM [toTVr assumps (toName Val v) | v <- hsDeclFreeVars pr ] $ \tvr -> do
+            cs <- flip mapM [toTVr assumps (toName Val v) | (v,_) <- hsDeclFreeVars pr ] $ \tvr -> do
hunk ./E/FromHs.hs 343
+applyCoersion :: Monad m => CoerceTerm -> E -> Ce m E
+applyCoersion CTId e = return e
+applyCoersion ct e = etaReduce `liftM` f ct e where
+    f CTId e = return e
+    f (CTAp ts) e = return $ foldl eAp e (map tipe ts)
+    f (CTAbs ts) e = return $ foldr eLam e (map fromTyvar ts)
+    f (CTCompose ct1 ct2) e = f ct1 =<< (f ct2 e)
+    f (CTFun CTId) e = return e
+    f (CTFun ct) e = do
+        let EPi TVr { tvrType = ty } _ = getType e
+        [y] <- newVars [ty]
+        fgy <- f ct (EAp e (EVar y))
+        return (eLam y fgy)
hunk ./E/FromHs.hs 456
-    cExpr (HsAsPat n' (HsVar n)) = return $ foldl eAp (EVar (tv n)) (map tipe $ specialize t t') where
-        t = getAssump n
-        t' = getAssump n'
+    cExpr (HsAsPat n' (HsVar n)) = do
+        cv <- lookupCoercion (toName Val n')
+        let t = getAssump n
+        case cv of
+            Left t' -> return $ foldl eAp (EVar (tv n)) (map tipe $ specialize t t')
+            Right c -> applyCoersion c $ EVar (tv n)
hunk ./FrontEnd/Tc/Main.hs 75
+tiExpr (HsAsPat n (HsVar v)) typ = do
+    sc <- lookupName (toName Val v)
+    f <- sc `subsumes` typ
+    addCoerce (toName Val n) f
+    return (HsAsPat n $ HsVar v)
+
+{-
+-- TODO should subsume for rank-n
hunk ./FrontEnd/Tc/Main.hs 87
-
+-}
hunk ./FrontEnd/Tc/Main.hs 473
-        dv n = do
+        dv (n,Nothing) = do
hunk ./FrontEnd/Tc/Main.hs 478
+        dv (n,Just t) = do
+            kt <- getKindEnv
+            tt <- hsTypeToType kt t
+            let env = (Map.singleton (toName Val n) tt)
+            addToCollectedEnv env
+            return (tt,env)
hunk ./FrontEnd/Tc/Type.hs 332
+    deriving(Show)
+
+ctFun CTId = CTId
+ctFun x = CTFun x
+ctAbs [] = CTId
+ctAbs xs = CTAbs xs
+ctAp [] = CTId
+ctAp xs = CTAp xs
+ctId = CTId
hunk ./FrontEnd/Tc/Type.hs 343
+composeCoerce (CTFun a) (CTFun b) = ctFun (a `composeCoerce` b)
hunk ./FrontEnd/Tc/Type.hs 346
+composeCoerce (CTAbs ts) (CTAbs ts') = CTAbs (ts ++ ts')
+composeCoerce (CTAp ts) (CTAp ts') = CTAp (ts ++ ts')
+--composeCoerce (CTAbs ts) (CTAp ts') = f ts ts' where
+--    f (t:ts) (TVar t':ts') | t == t' = f ts ts'
+--    f [] [] = CTId
+--    f _ _ = CTCompose (CTAbs ts) (CTAp ts')
hunk ./FrontEnd/Tc/Unify.hs 18
-ctId = CTId
hunk ./FrontEnd/Tc/Unify.hs 50
-        return (composeCoerce (CTAbs vs) f)
+        return (composeCoerce (ctAbs vs) f)
hunk ./FrontEnd/Tc/Unify.hs 58
-        return (f `composeCoerce` (CTAp ts))
+        return (f `composeCoerce` (ctAp ts))
hunk ./FrontEnd/Tc/Unify.hs 71
-        return (CTFun f2)
+        return (ctFun f2)