[fix type checker bug that occasionally reported false erros
John Meacham <john@repetae.net>**20101206120451
 Ignore-this: a34be6e294bde1e95ad7a9ca35b42055
] hunk ./src/E/Eval.hs 9
+--import Debug.Trace
hunk ./src/E/Eval.hs 17
+trace _ x = x
hunk ./src/E/Eval.hs 19
-
+-- evaluate to WHNF
hunk ./src/E/Eval.hs 56
-strong dsMap' term = eval' dsMap term [] where
+strong dsMap' term = trace ("strong: " ++ show term) $ eval' dsMap term [] where
hunk ./src/E/Eval.hs 58
-    --eval' ds t@EVar {} [] = t
hunk ./src/E/Eval.hs 61
-    eval' :: Monad m => Map.Map TVr E -> E -> [E] -> m E
hunk ./src/E/Eval.hs 62
+    eval' :: Monad m => Map.Map TVr E -> E -> [E] -> m E
hunk ./src/E/Eval.hs 87
-        | Just x <- Map.lookup v ds = eval' ds x stack
+        | Just x <- Map.lookup v ds = trace ("strong-lookup: " ++ show v) $ eval' ds x stack
hunk ./src/E/Eval.hs 103
-                                      <$> pprint (Map.keys ds)
+                                      <$> pprint ds
hunk ./src/E/Lint.hs 1
-module E.Lint where
+module E.Lint(
+    transformProgram,
+    onerrNone,
+    lintCheckProgram,
+    dumpCore
+    ) where
hunk ./src/E/Lint.hs 11
-import qualified Data.Set as Set
hunk ./src/E/Lint.hs 14
-
+import qualified Data.Set as Set
hunk ./src/E/Lint.hs 35
-
hunk ./src/E/Lint.hs 63
---            printProgram prog
hunk ./src/E/Lint.hs 65
-            dumpCore ("lint-after-" ++ name) prog'
+            let fvs = programFreeVars prog' `mappend` programFreeVars prog
+                rtvrs = "FreeVars:\n" ++ (render $ vcat $ map (\tvr -> hang 4 (pprint (tvr :: TVr) <+> text "::" <+> (pprint $ tvrType tvr))) fvs)
+            dumpCoreExtra ("lint-after-" ++ name) prog' rtvrs
hunk ./src/E/Lint.hs 131
-        --putErrLn (show ids)
hunk ./src/E/Lint.hs 134
+programFreeVars prog = freeVars (ELetRec (programDs prog) Unknown)
hunk ./src/E/Main.hs 207
+        lintCheckProgram onerrNone mprog
hunk ./src/E/Main.hs 209
+        lintCheckProgram onerrNone mprog
hunk ./src/E/TypeCheck.hs 64
-subsumes both term and type level abstractions. 
+subsumes both term and type level abstractions.
hunk ./src/E/TypeCheck.hs 69
-evaluates to a function. 
+evaluates to a function.
hunk ./src/E/TypeCheck.hs 78
-    as a shortcut we will use *# to mean every combination involving * and #, and so forth. 
+    as a shortcut we will use *# to mean every combination involving * and #, and so forth.
hunk ./src/E/TypeCheck.hs 109
-representation. Due to this, functions may be written that are polymorphic in types of these kinds. 
+representation. Due to this, functions may be written that are polymorphic in types of these kinds.
hunk ./src/E/TypeCheck.hs 153
-          /\     \    | 
+          /\     \    |
hunk ./src/E/TypeCheck.hs 253
-    rfc e =  withContextDoc (text "fullCheck:" </> prettyE e) (fc e >>=  strong')
-    rfc' nds e = withContextDoc (text "fullCheck:" </> prettyE e) (inferType' nds e >>=  strong')
-    strong' e = withContextDoc (text "Strong:" </> prettyE e) $ strong ds e
+    rfc e =  withContextDoc (text "fullCheck:" </> prettyE e) (fc e >>= strong')
+    rfc' nds e = withContextDoc (text "fullCheck':" </> prettyE e) (inferType' nds e)
+    strong' e = withContextDoc (parens $ text "Strong:" </> prettyE e) $ strong ds e
hunk ./src/E/TypeCheck.hs 286
+        withContext "Checking Lambda" $ do
hunk ./src/E/TypeCheck.hs 288
-        b' <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
-        strong' $ EPi tvr b'
+        b' <- withContext "Checking Lambda Body" $ rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
+        withContext "Checking lambda pi" $ strong' $ EPi tvr b'
hunk ./src/E/TypeCheck.hs 291
-    fc (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = fc (EAp (foldl eAp af (litArgs lc)) b)
+    fc (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = rfc (EAp (foldl eAp af (litArgs lc)) b)
hunk ./src/E/TypeCheck.hs 305
-        et <- inferType' nds e
-        strong nds et
+        inferType' nds e
+        --et <- inferType' nds e
+        --strong nds et
hunk ./src/E/TypeCheck.hs 311
+        withContext "Checking typelike pattern binding case" $ do
hunk ./src/E/TypeCheck.hs 320
+        withContext "Checking typelike binding case" $ do
hunk ./src/E/TypeCheck.hs 328
-        ps <- mapM (strong' . getType) $ casePats ec
+        ps <- withContext "Getting pattern types" $ mapM (strong' . getType) $ casePats ec
hunk ./src/E/TypeCheck.hs 330
-        strong' dt
+        withContext "Evaluating Case Type" $ strong' dt
hunk ./src/E/TypeCheck.hs 332
+        withContext "Checking plain case" $ do
hunk ./src/E/TypeCheck.hs 384
-        Left ss -> fail $ "\n>>> internal error:\n" ++ unlines (tail ss)
+        Left ss -> fail $ "\n>>> internal error:\n" ++ unlines ss
hunk ./src/E/TypeCheck.hs 469
-    rfc e =  withContextDoc (text "fullCheck':" </> ePretty e) (fc e >>=  strong')
-    rfc' nds e =  withContextDoc (text "fullCheck':" </> ePretty e) (inferType' nds  e >>=  strong')
+    rfc e =  withContextDoc (text "fullCheck':" </> ePretty e) (fc e >>= strong')
+    rfc' nds e =  withContextDoc (text "fullCheck':" </> ePretty e) (inferType' nds e)
hunk ./src/E/TypeCheck.hs 494
-        et <- inferType' nds e
-        strong nds et
+        --et <- inferType' nds e
+        --strong nds et
+        inferType' nds e