[use declarations after they have be rewritten by the typechecker, have the typechecker insert coercions wherever it pleases, generalize on skolomization properly.
John Meacham <john@repetae.net>**20060303045214] hunk ./FrontEnd/TI/Module.hs 280
+            tiCoerce = mempty,
+            tiDataDecls = mempty,
hunk ./FrontEnd/Tc/Main.hs 45
-tcApps e as typ = do
+tcKnownApp e nname vname as typ = do
+    sc <- lookupName vname
+    let (_,_,rt) = fromType sc
+    -- fall through if the type isn't arrowy enough (will produce type error)
+    if (length . fst $ fromTArrow rt) < length as then tcApps' e as typ else do
+    (ts,rt) <- freshInstance Sigma sc
+    addCoerce nname (ctAp ts)
+    let f (TArrow x y) (a:as) = do
+            a <- tcExprPoly a x
+            y <- findType y
+            (as,fc) <- f y as
+            return (a:as,fc)
+        f lt [] = do
+            fc <- lt `subsumes` typ
+            return ([],fc)
+    (nas,CTId) <- f rt as
+    return (e,nas)
+
+tcApps e@(HsAsPat n (HsVar v)) as typ = do
+    let vname = toName Val v
+    let nname = toName Val n
+    when (dump FD.BoxySteps) $ liftIO $ putStrLn $ "tcApps: " ++ (show nname ++ "@" ++ show vname)
+    rc <- asks tcRecursiveCalls
+    -- fall through if this is a recursive call to oneself
+    if (vname `Set.member` rc) then tcApps' e as typ else do
+    tcKnownApp e nname vname as typ
+
+tcApps e@(HsAsPat n (HsCon v)) as typ = do
+    let vname = toName DataConstructor v
+    let nname = toName Val n
+    when (dump FD.BoxySteps) $ liftIO $ putStrLn $ "tcApps: " ++ (show nname ++ "@" ++ show vname)
+    addToCollectedEnv (Map.singleton (toName Val n) typ)
+    tcKnownApp e nname vname as typ
+
+tcApps e as typ = tcApps' e as typ
+
+-- the fall through case
+tcApps' e as typ = do
hunk ./FrontEnd/Tc/Main.hs 89
+
hunk ./FrontEnd/Tc/Main.hs 102
-    --(_,_,t) <- skolomize t
-    tcExpr e t
+    (ts,_,t) <- skolomize t
+    e <- tcExpr e t
+    doCoerce (ctAbs ts) e
+
+doCoerce :: CoerceTerm -> HsExp -> Tc HsExp
+doCoerce CTId e = return e
+doCoerce ct e = do
+    nn <- newUniq
+    let n = toName Val ("As@",show nn)
+    addCoerce n ct
+    return (HsAsPat (nameName n) e)
+
hunk ./FrontEnd/Tc/Main.hs 226
-            --(_,_,s) <- skolomize s
-            lam ps e s rs
-
-
+            (ts,_,s) <- skolomize s
+            e <- lam ps e s rs
+            doCoerce (ctAbs ts) e
hunk ./FrontEnd/Tc/Main.hs 239
-    (HsCon _,exps') <- tcApps (HsCon (toTuple (length exps))) exps typ
+    (_,exps') <- tcApps (HsCon (toTuple (length exps))) exps typ
hunk ./FrontEnd/Tc/Main.hs 616
-        lam (p:ps) (TArrow s1' s2') rs = do -- ABS1
-            --box <- newBox Star
+        lam (p:ps) ty@(TArrow s1' s2') rs = do -- ABS1
hunk ./FrontEnd/Tc/Main.hs 618
-            --s1' `boxyMatch` box
-            --liftIO $ print (p',env)
hunk ./FrontEnd/Tc/Main.hs 620
-                lamPoly ps s2' (p':rs)  -- TODO poly
+                lamPoly ps s2' (p':rs)
hunk ./FrontEnd/Tc/Main.hs 630
-            --(_,_,s) <- skolomize s
+            (_,_,s) <- skolomize s
hunk ./FrontEnd/Tc/Main.hs 633
-    lam pats typ []
+    res <- lam pats typ []
+    return res
hunk ./FrontEnd/Tc/Main.hs 728
-        liftIO $ print ps
hunk ./FrontEnd/Tc/Main.hs 744
-        ((),ps) <- listenPreds $ mapM_ tcPragmaDecl es
+        (pdecls,ps) <- listenPreds $ mapM tcPragmaDecl es
hunk ./FrontEnd/Tc/Main.hs 749
-        return rs
+        return (rs ++ concat pdecls)
hunk ./FrontEnd/Tc/Module.hs 221
-    (localVarEnv,checkedRules,coercions) <- withOptionsT (modInfoOptions tms) $ runTc tcInfo $ do
+    (localVarEnv,checkedRules,coercions,ds) <- withOptionsT (modInfoOptions tms) $ runTc tcInfo $ do
hunk ./FrontEnd/Tc/Module.hs 229
-        return (env,checkedRules out,cc')
+        return (env,checkedRules out,cc',ds)
+
+    when (dump FD.Renamed) $ do
+        putStrLn " \n ---- typechecked code ---- \n"
+        mapM_ (putStrLn . HsPretty.render . HsPretty.ppHsDecl) ds
hunk ./FrontEnd/Tc/Module.hs 264
-            tiDataLiftedInstances = Map.fromList [ (getDeclName d,d) | d <- liftedInstances],
+            --tiDataLiftedInstances = Map.fromList [ (getDeclName d,d) | d <- liftedInstances],
+            tiDataLiftedInstances = error "tiDataLiftedInstances not used", -- Map.fromList [ (getDeclName d,d) | d <- ds],
+            tiDataDecls = ds,
hunk ./FrontEnd/TiData.hs 14
+    tiDataDecls      :: [HsDecl],
hunk ./Main.hs 173
-        decls = concat [ hsModuleDecls  m | (_,m) <- tiDataModules tiData ] ++ Map.elems (tiDataLiftedInstances tiData)
+        decls | fopts FO.Boxy = tiDataDecls tiData
+              | otherwise = concat [ hsModuleDecls  m | (_,m) <- tiDataModules tiData ] ++ Map.elems (tiDataLiftedInstances tiData)
+        originalDecls =  concat [ hsModuleDecls  m | (_,m) <- tiDataModules tiData ]
hunk ./Main.hs 178
-    let dataTable = toDataTable (getConstructorKinds (hoKinds ho')) (tiAllAssumptions tiData) decls
+    let dataTable = toDataTable (getConstructorKinds (hoKinds ho')) (tiAllAssumptions tiData) originalDecls
hunk ./Main.hs 192
-    mapM_ (\(_,v,lc) -> printCheckName'' fullDataTable v lc) ds
+    --mapM_ (\(_,v,lc) -> printCheckName'' fullDataTable v lc) ds
hunk ./Main.hs 310
-    wdump FD.Lambdacube $ printProgram prog
hunk ./Main.hs 399
+    wdump FD.Lambdacube $ printProgram prog