From 3f72d28b7b348d441dde0e66e848ed4d7c16f5ba Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 18 Nov 2024 17:04:21 +0000 Subject: Better type errors within lets. --- src/Inky/Term/Pretty/Error.idr | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/Inky/Term/Pretty') 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 -- cgit v1.2.3