From 5c9b102c15ce92f0f86dd1e2f468c01b870d94a2 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Thu, 13 Oct 2022 11:57:03 +0300
Subject: [PATCH 1/2] Pretty printing for Core Lint errors

---
 src/Cryptol/ModuleSystem/Base.hs |   6 +-
 src/Cryptol/TypeCheck/Sanity.hs  | 120 ++++++++++++++++++++++++++++++-
 2 files changed, 124 insertions(+), 2 deletions(-)

diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index c574a9771..cc788b52a 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -574,7 +574,11 @@ typecheck act i params env = do
                            Right as ->
                              let ppIt l = mapM_ (logPrint l . T.pp)
                              in withLogger ppIt as
-                           Left err -> panic "Core lint failed:" [show err]
+                           Left (loc,err) ->
+                            panic "Core lint failed:"
+                              [ "Location: " ++ show (T.pp loc)
+                              , show (T.pp err)
+                              ]
          return o
 
     T.InferFailed nameMap warns errs ->
diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs
index 8a89ce8c8..bacdf8d7a 100644
--- a/src/Cryptol/TypeCheck/Sanity.hs
+++ b/src/Cryptol/TypeCheck/Sanity.hs
@@ -5,6 +5,7 @@
 -- Maintainer  :  cryptol@galois.com
 -- Stability   :  provisional
 -- Portability :  portable
+{-# Language OverloadedStrings #-}
 module Cryptol.TypeCheck.Sanity
   ( tcExpr
   , tcDecls
@@ -19,8 +20,10 @@ import Cryptol.Parser.Position(thing,Range,emptyRange)
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst)
 import Cryptol.TypeCheck.Monad(InferInput(..))
+import Cryptol.ModuleSystem.Name(nameLoc)
 import Cryptol.Utils.Ident
 import Cryptol.Utils.RecordMap
+import Cryptol.Utils.PP
 
 import Data.List (sort)
 import qualified Data.Set as Set
@@ -410,7 +413,11 @@ checkDecl checkSig d =
          when checkSig $ checkSchema s
          s1 <- exprSchema e
          unless (same s s1) $
-           reportError $ TypeMismatch "DExpr" s s1
+           let nm = dName d
+               loc = "definition of " ++ show (pp nm) ++
+                              ", at " ++ show (pp (nameLoc nm))
+           in reportError $ TypeMismatch loc s s1
+  
          return (dName d, s)
 
 checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
@@ -586,3 +593,114 @@ lookupVar x =
      case Map.lookup x (roVars ro) of
        Just s -> return s
        Nothing -> reportError $ UndefinedVariable x
+
+
+instance PP Error where
+  ppPrec _ err =
+    case err of
+
+      TypeMismatch what expected actual ->
+        ppErr ("Type mismatch in" <+> text what)
+          [ "Expected:" <+> pp expected
+          , "Actual  :" <+> pp actual
+          ]
+
+      ExpectedMono s ->
+        ppErr "Not a monomorphic type"
+          [ pp s ]
+
+      TupleSelectorOutOfRange sel sz ->
+        ppErr "Tuple selector out of range"
+          [ "Selector:" <+> int sel
+          , "Size    :" <+> int sz
+          ]
+
+      MissingField f fs ->
+        ppErr "Invalid record selector"
+          [ "Field: " <+> pp f
+          , "Fields:" <+> commaSep (map pp fs)
+          ]
+
+      UnexpectedTupleShape expected actual ->
+        ppErr "Unexpected tuple shape"
+          [ "Expected:" <+> int expected
+          , "Actual  :" <+> int actual
+          ]
+
+      UnexpectedRecordShape expected actual ->
+        ppErr "Unexpected record shape"
+          [ "Expected:" <+> commaSep (map pp expected)
+          , "Actual  :" <+> commaSep (map pp actual)
+          ]
+
+      UnexpectedSequenceShape n t ->
+        ppErr "Unexpected sequence shape"
+          [ "Expected:" <+> int n
+          , "Actual  :" <+> pp t
+          ]
+
+      BadSelector sel t ->
+        ppErr "Bad selector"
+          [ "Selector:" <+> pp sel
+          , "Type    :" <+> pp t
+          ]
+
+      BadInstantiation ->
+        ppErr "Bad instantiation" []
+
+      Captured x ->
+        ppErr "Captured typed variable"
+          [ "Variable:" <+> pp x ]
+
+      BadProofNoAbs ->
+        ppErr "Proof application without a proof abstraction" []
+
+      BadProofTyVars xs ->
+        ppErr "Proof application with type abstraction"
+          [ "Type parameter:" <+> pp x | x <- xs ]
+
+      KindMismatch expected actual ->
+        ppErr "Kind mismatch"
+          [ "Expected:" <+> pp expected
+          , "Actual  :" <+> pp actual
+          ]
+
+      NotEnoughArgumentsInKind k ->
+        ppErr "Not enough arguments in kind" [ pp k ]
+
+      BadApplication t1 t2 ->
+        ppErr "Bad application"
+          [ "Function:" <+> pp t1
+          , "Argument:" <+> pp t2
+          ]
+
+      FreeTypeVariable x ->
+        ppErr "Free type variable"
+          [ "Variable:" <+> pp x ]
+
+      BadTypeApplication kf ka ->
+        ppErr "Bad type application"
+          [ "Function :" <+> pp kf
+          , "Arguments:" <+> commaSep (map pp ka)
+          ]
+
+      RepeatedVariableInForall x ->
+        ppErr "Repeated variable in forall"
+          [ "Variable:" <+> pp x ]
+
+      BadMatch t ->
+        ppErr "Bad match"
+          [ "Type:" <+> pp t ]
+
+      EmptyArm -> ppErr "Empty comprehension arm" []
+
+      UndefinedTypeVaraible x ->
+        ppErr "Undefined type variable"
+          [ "Variable:" <+> pp x ]
+
+      UndefinedVariable x ->
+        ppErr "Undefined variable"
+          [ "Variable:" <+> pp x ]
+
+    where
+    ppErr x ys = hang x 2 (vcat [ "•" <+> y | y <- ys ])

From 080b40ba352999c3fa165b3abe0fea2ab5f387c4 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Thu, 13 Oct 2022 17:54:58 +0300
Subject: [PATCH 2/2] Fix typo

---
 src/Cryptol/TypeCheck/Sanity.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs
index bacdf8d7a..8dc27c61a 100644
--- a/src/Cryptol/TypeCheck/Sanity.hs
+++ b/src/Cryptol/TypeCheck/Sanity.hs
@@ -649,7 +649,7 @@ instance PP Error where
         ppErr "Bad instantiation" []
 
       Captured x ->
-        ppErr "Captured typed variable"
+        ppErr "Captured type variable"
           [ "Variable:" <+> pp x ]
 
       BadProofNoAbs ->