Better type errors within lets.

3 files changed, 35 insertions, 0 deletions

diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index d6ec466..54ac9fe 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -418,6 +418,11 @@ data NotSynths where
   LetNS1 :
     NotSynths tyEnv tmEnv e ->
     NotSynths tyEnv tmEnv (Let meta e (x ** f))
+  LetNS2' :
+    These
+      (NotSynths tyEnv tmEnv (Annot meta' e a))
+      (NotSynths tyEnv (tmEnv :< (x :- sub tyEnv a)) f) ->
+    NotSynths tyEnv tmEnv (Let meta (Annot meta' e a) (x ** f))
   LetNS2 :
     Synths tyEnv tmEnv e a ->
     NotSynths tyEnv (tmEnv :< (x :- a)) f ->
@@ -470,6 +475,11 @@ data NotChecks where
   LetNC1 :
     NotSynths tyEnv tmEnv e ->
     NotChecks tyEnv tmEnv b (Let meta e (x ** t))
+  LetNC2' :
+    These
+      (NotSynths tyEnv tmEnv (Annot meta' e a))
+      (NotChecks tyEnv (tmEnv :< (x :- sub tyEnv a)) b t) ->
+    NotChecks tyEnv tmEnv b (Let meta (Annot meta' e a) (x ** t))
   LetNC2 :
     Synths tyEnv tmEnv e a ->
     NotChecks tyEnv (tmEnv :< (x :- a)) b t ->
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 8de671c..402f623 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -63,6 +63,9 @@ synthsSplit (AnnotS wf prf) (AnnotNS contras) =
   these (wellFormedSplit wf) (checksSplit prf) (const $ checksSplit prf) contras
 synthsSplit VarS contra = absurd contra
 synthsSplit (LetS prf1 prf2) (LetNS1 contra) = synthsSplit prf1 contra
+synthsSplit (LetS prf1 prf2) (LetNS2' (This contra)) = synthsSplit prf1 contra
+synthsSplit (LetS (AnnotS wf prf1) prf2) (LetNS2' (That contra)) = synthsSplit prf2 contra
+synthsSplit (LetS prf1 prf2) (LetNS2' (Both contra1 contra2)) = synthsSplit prf1 contra1
 synthsSplit (LetS prf1 prf2) (LetNS2 prf1' contra) =
   let contra = rewrite synthsUnique prf1 prf1' in contra in
   synthsSplit prf2 contra
@@ -113,6 +116,9 @@ checksSplit (MapC prf1 prf2) (EmbedNC2 Map prf1' contra) =
   let contra = rewrite synthsUnique prf1 prf1' in contra in
   alphaSplit prf2 contra
 checksSplit (LetC prf1 prf2) (LetNC1 contra) = synthsSplit prf1 contra
+checksSplit (LetC prf1 prf2) (LetNC2' (This contra)) = synthsSplit prf1 contra
+checksSplit (LetC (AnnotS wf prf1) prf2) (LetNC2' (That contra)) = checksSplit prf2 contra
+checksSplit (LetC prf1 prf2) (LetNC2' (Both contra1 contra2)) = synthsSplit prf1 contra1
 checksSplit (LetC prf1 prf2) (LetNC2 prf1' contra) =
   let contra = rewrite synthsUnique prf1 prf1' in contra in
   checksSplit prf2 contra
@@ -238,6 +244,11 @@ synths tyEnv tmEnv (Annot _ t a) =
   map (uncurry AnnotS) AnnotNS $
   all (wellFormed a) (checks tyEnv tmEnv (sub tyEnv a) t)
 synths tyEnv tmEnv (Var _ i) = Just (indexAll i.pos tmEnv).value `Because` VarS
+synths tyEnv tmEnv (Let _ (Annot _ e a) (x ** t)) =
+  map id (\_ => uncurry (LetS . uncurry AnnotS)) (LetNS2' . mapFst AnnotNS) $
+  all
+    (all (wellFormed a) (checks tyEnv tmEnv (sub tyEnv a) e))
+    (synths tyEnv (tmEnv :< (x :- sub tyEnv a)) t)
 synths tyEnv tmEnv (Let _ e (x ** f)) =
   map snd
     (\(_, _), (prf1, prf2) => LetS prf1 prf2)
@@ -309,6 +320,11 @@ synths tyEnv tmEnv (Map _ (x ** a) b c) =
 
 checks tyEnv tmEnv a (Annot meta t b) = fallbackCheck Annot (synths tyEnv tmEnv $ Annot meta t b) a
 checks tyEnv tmEnv a (Var meta i) = fallbackCheck Var (synths tyEnv tmEnv $ Var meta i) a
+checks tyEnv tmEnv a (Let _ (Annot _ e b) (x ** t)) =
+  map (uncurry (LetC . uncurry AnnotS)) (LetNC2' . mapFst AnnotNS) $
+  all
+    (all (wellFormed b) (checks tyEnv tmEnv (sub tyEnv b) e))
+    (checks tyEnv (tmEnv :< (x :- sub tyEnv b)) a t)
 checks tyEnv tmEnv a (Let _ e (x ** t)) =
   map
     (\(_ ** (prf1, prf2)) => LetC prf1 prf2)
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr
index 651d208..a5ee2fa 100644
--- a/src/Inky/Term/Pretty/Error.idr
+++ b/src/Inky/Term/Pretty/Error.idr
@@ -73,6 +73,10 @@ prettyNotSynths (AnnotNS {a} (Both contra1 contra2)) =
   (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
   prettyNotChecks contra2
 prettyNotSynths (LetNS1 contra) = prettyNotSynths contra
+prettyNotSynths (LetNS2' (This contra)) = prettyNotSynths contra
+prettyNotSynths (LetNS2' (That contra)) = prettyNotSynths contra
+prettyNotSynths (LetNS2' (Both contra1 contra2)) =
+  prettyNotSynths contra1 ++ prettyNotSynths contra2
 prettyNotSynths (LetNS2 prf contra) =
   case synthsRecompute prf of
     Val a => prettyNotSynths contra
@@ -130,6 +134,11 @@ prettyNotChecks (EmbedNC2 _ prf contra) =
         prettyType b Open
       )]
 prettyNotChecks (LetNC1 contra) = prettyNotSynths contra
+prettyNotChecks (LetNC2' (This contra)) = prettyNotSynths contra
+prettyNotChecks (LetNC2' (That contra)) = prettyNotChecks contra
+prettyNotChecks (LetNC2' (Both contra1 contra2)) =
+  prettyNotSynths contra1 ++
+  prettyNotChecks contra2
 prettyNotChecks (LetNC2 prf contra) =
   case synthsRecompute prf of
     Val _ => prettyNotChecks contra