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.idr | |
| parent | 6cb440c405868bc1740534731153f877209a325d (diff) | |
Better type errors within lets.
Diffstat (limited to 'src/Inky/Term.idr')
| -rw-r--r-- | src/Inky/Term.idr | 10 |
1 files changed, 10 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 -> |