diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-18 17:04:21 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-18 17:04:21 +0000 |
| commit | 3f72d28b7b348d441dde0e66e848ed4d7c16f5ba (patch) | |
| tree | b37acc42fd478d307a4e999275b684fea3927d9c /src/Inky/Term/Pretty | |
| parent | 6cb440c405868bc1740534731153f877209a325d (diff) | |
Better type errors within lets.
Diffstat (limited to 'src/Inky/Term/Pretty')
| -rw-r--r-- | src/Inky/Term/Pretty/Error.idr | 9 |
1 files changed, 9 insertions, 0 deletions
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 |