Browse Source

Add some context to type errors

hydraz 2 years ago
parent
commit
954c02672b
3 changed files with 22 additions and 9 deletions
  1. 6 3
      src/Main.hs
  2. 2 0
      src/Types/Context.hs
  3. 14 6
      src/Types/Infer.hs

+ 6 - 3
src/Main.hs

@@ -42,12 +42,12 @@ main = do
                                        (prettyPrint term) (prettyPrint typ)
 
 printErr :: TypeError -> IO ()
-printErr (Redefinition v) = printf "Redefinition of %s" (prettyPrint v)
+printErr (Redefinition v) = printf "Redefinition of %s\n" (prettyPrint v)
 printErr (NotFound Infer _ v) =
-  printf "Variable %s not in scope during inference."
+  printf "Variable %s not in scope during inference.\n"
          (prettyPrint v)
 printErr (NotFound Normal _ v) =
-  printf "Variable %s not in scope during normalisation."
+  printf "Variable %s not in scope during normalisation.\n"
          (prettyPrint v)
 printErr (ExpectedType t) = printf "Expected type, got %s\n" (prettyPrint t)
 printErr (ExpectedPi t) = printf "Expected Pi-type, got %s\n" (prettyPrint t)
@@ -65,3 +65,6 @@ printErr (Unexhaustive t) = printf "Unexhaustive match: %s\n" (prettyPrint t)
 printErr (DueTo a b) = do
   printErr a
   putStr " · " *> printErr b
+printErr (Here a b) = do
+  printErr b
+  printf " · While verifying correctness of %s\n" (prettyPrint a)

+ 2 - 0
src/Types/Context.hs

@@ -112,7 +112,9 @@ data TypeError
 
   | Redefinition Var
   | Unexhaustive Term
+
   | DueTo TypeError TypeError
+  | Here Term TypeError
   deriving (Show)
 
 data Phase = Infer | Normal deriving (Show)

+ 14 - 6
src/Types/Infer.hs

@@ -20,6 +20,8 @@ import Control.Monad.Freer
 import Data.These
 
 import Control.Monad
+import Debug.Trace
+import Pretty(prettyPrint)
 
 infer :: ( Member (Exc TypeError) r
          , Member (Reader Context) r
@@ -118,8 +120,7 @@ assertEquality :: ( Member Fresh r
                => Type -> Type -> Eff r ()
 assertEquality t1 t2 = do
  cs <- U.unify t1 t2
- solve infer inferSet cs `catchError`
-   (throwError . DueTo (NotEqual t1 t2))
+ solve infer inferSet cs
 
 inferSet :: ( Member (Exc TypeError) r
             , Member (Reader Context) r
@@ -128,6 +129,7 @@ inferSet :: ( Member (Exc TypeError) r
 inferSet t = do
   x <- infer t
   x' <- N.normalise x
+  trace (show t ++ " : " ++ show x') (pure ())
   case x' of
     Set k -> pure k
     x -> throwError (ExpectedType x)
@@ -142,6 +144,7 @@ checkProgram (Postulate v t:xs) = do
   case x of
     Just _ -> throwError (Redefinition v)
     Nothing -> local (insertType (v, t)) $ checkProgram xs
+
 checkProgram (DataDecl i@(MkInductive in' it _):xs) = do
   x <- ask
   case insertInductive i x of
@@ -150,11 +153,14 @@ checkProgram (DataDecl i@(MkInductive in' it _):xs) = do
       local (insertType (in', it)) $
         forM_ ins $ \(v, t) ->
           if v /= in'
-             then void (inferSet t)
+             then void (inferSet t) `catchError`
+                 (throwError . Here (Variable v))
              else pure ()
       local (const vl) $ checkProgram xs
+
 checkProgram (Define v vl:xs) = do
-  ty <- infer vl
+  ty <- infer vl `catchError`
+          (throwError . Here (Variable v) . Here vl)
   lt <- lookupType v
   case lt of
     Just t -> do
@@ -171,11 +177,13 @@ checkProgram [Eval t] = do
         t' `assertEquality` t
       _ -> pure ()
   vl <- N.fixpointNorm t
-  tp <- infer t
+  tp <- infer t `catchError`
+    (throwError . Here t)
   pure (ctx, Just (vl, tp))
 
 checkProgram (Eval t:xs) = do
-  _ <- infer t
+  _ <- infer t `catchError`
+    (throwError . Here t)
   checkProgram xs
 
 checkProgram [] = do