1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
|
module Inky.Term.Pretty.Error
import Data.List.Quantifiers
import Data.Singleton
import Data.String
import Data.These
import Flap.Decidable.Maybe
import Inky.Term
import Inky.Term.Recompute
import Inky.Type.Pretty
import Text.PrettyPrint.Prettyprinter
-- Typing Errors ---------------------------------------------------------------
Pretty (ChecksOnly t) where
pretty Abs = "abstraction"
pretty Inj = "injection"
pretty Case = "case split"
pretty Roll = "rolling"
pretty Fold = "fold"
export
prettyNotSynths :
{tyCtx, tmCtx : SnocList String} ->
{e : Term NoSugar m tyCtx tmCtx} ->
{tyEnv : _} -> {tmEnv : _} ->
NotSynths tyEnv tmEnv e ->
List (m, Doc ann)
export
prettyNotChecks :
{tyCtx, tmCtx : SnocList String} ->
{a : Ty [<]} ->
{t : Term NoSugar m tyCtx tmCtx} ->
{tyEnv : _} -> {tmEnv : _} ->
NotChecks tyEnv tmEnv a t ->
List (m, Doc ann)
prettyNotCheckSpine :
{tyCtx, tmCtx : SnocList String} ->
{a : Ty [<]} ->
{ts : List (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : _} -> {tmEnv : _} ->
NotCheckSpine tyEnv tmEnv a ts ->
List (m, Doc ann)
prettyAnyNotSynths :
{tyCtx, tmCtx : SnocList String} ->
{es : Context (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : _} -> {tmEnv : _} ->
AnyNotSynths tyEnv tmEnv es ->
List (m, Doc ann)
prettyAnyNotChecks :
{tyCtx, tmCtx : SnocList String} ->
{ts : Context (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : _} -> {tmEnv : _} -> {as : Context _} ->
(meta : m) ->
AnyNotChecks tyEnv tmEnv as ts ->
List (m, Doc ann)
prettyAnyNotBranches :
{tyCtx, tmCtx : SnocList String} ->
{ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))} ->
{tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} ->
(meta : m) ->
AnyNotBranches tyEnv tmEnv as a ts ->
List (m, Doc ann)
prettyNotSynths (ChecksNS shape) =
[(e.meta, pretty "cannot synthesise type of" <++> pretty shape)]
prettyNotSynths (AnnotNS {a} (This contra)) =
[(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
prettyNotSynths (AnnotNS (That contra)) = prettyNotChecks contra
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
prettyNotSynths (LetTyNS {a} (This contra)) =
[(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
prettyNotSynths (LetTyNS (That contra)) = prettyNotSynths contra
prettyNotSynths (LetTyNS {a} (Both contra1 contra2)) =
(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)
:: prettyNotSynths contra2
prettyNotSynths (AppNS1 contra) = prettyNotSynths contra
prettyNotSynths (AppNS2 prf contras) =
case synthsRecompute prf of
Val a => prettyNotCheckSpine contras
prettyNotSynths (TupNS contras) = prettyAnyNotSynths contras
prettyNotSynths (PrjNS1 contra) = prettyNotSynths contra
prettyNotSynths (PrjNS2 prf f) =
case synthsRecompute prf of
Val a =>
[(e.meta
, pretty "cannot project non-product type" <+> line <+>
prettyType a Open
)]
prettyNotSynths (PrjNS3 {l, e, as} prf contra) =
case synthsRecompute prf of
Val (TProd as) =>
[(e.meta
, pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
pretty "in product type" <+> line <+>
prettyType (TProd as) Open
)]
prettyNotSynths (UnrollNS1 contra) = prettyNotSynths contra
prettyNotSynths (UnrollNS2 prf contra) =
case synthsRecompute prf of
Val a =>
[(e.meta
, pretty "cannot unroll non-inductive type" <+> line <+>
prettyType a Open
)]
prettyNotSynths (MapNS {a} {b} {c} contras) =
bifoldMap
(const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
(bifoldMap
(const [(e.meta, pretty "ill-formed source" <+> line <+> prettyType b Open)])
(const [(e.meta, pretty "ill-formed target" <+> line <+> prettyType c Open)]))
contras
prettyNotChecks (EmbedNC1 _ contra) = prettyNotSynths contra
prettyNotChecks (EmbedNC2 _ prf contra) =
case synthsRecompute prf of
Val b =>
[(t.meta
, pretty "cannot unify" <+> line <+>
prettyType a Open <+> line <+>
pretty "and" <+> line <+>
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
prettyNotChecks (LetTyNC {a} (This contra)) =
[(t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
prettyNotChecks (LetTyNC (That contra)) = prettyNotChecks contra
prettyNotChecks (LetTyNC (Both contra1 contra2)) =
(t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
prettyNotChecks contra2
prettyNotChecks (AbsNC1 contra) =
[(t.meta, pretty "cannot abstract to construct type" <+> line <+> prettyType a Open)]
prettyNotChecks (AbsNC2 prf contra) =
case isFunctionRecompute prf of
(Val _, Val _) => prettyNotChecks contra
prettyNotChecks (TupNC1 contra) =
[(t.meta, pretty "cannot tuple to construct type" <+> line <+> prettyType a Open)]
prettyNotChecks (TupNC2 contras) = prettyAnyNotChecks t.meta contras
prettyNotChecks (InjNC1 contra) =
[(t.meta, pretty "cannot inject to construct type" <+> line <+> prettyType a Open)]
prettyNotChecks (InjNC2 {l} contra) =
[(t.meta
, pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
pretty "in sum type" <+> line <+>
prettyType a Open
)]
prettyNotChecks (InjNC3 i contra) =
case [| (nameOf i).value |] of
Val _ => prettyNotChecks contra
prettyNotChecks (CaseNC1 contra) = prettyNotSynths contra
prettyNotChecks (CaseNC2 prf contra) =
case synthsRecompute prf of
Val a => [(t.meta, pretty "cannot case split on type" <+> line <+> prettyType a Open)]
prettyNotChecks (CaseNC3 prf contras) =
case synthsRecompute prf of
Val _ => prettyAnyNotBranches t.meta contras
prettyNotChecks (RollNC1 contra) =
[(t.meta, pretty "cannot roll to construct type" <+> line <+> prettyType a Open)]
prettyNotChecks (RollNC2 contra) = prettyNotChecks contra
prettyNotChecks (FoldNC1 contra) = prettyNotSynths contra
prettyNotChecks (FoldNC2 prf contra) =
case synthsRecompute prf of
Val a => [(t.meta, pretty "cannot fold over type" <+> line <+> prettyType a Open)]
prettyNotChecks (FoldNC3 prf contra) =
case synthsRecompute prf of
Val _ => prettyNotChecks contra
prettyNotCheckSpine (Step1 {t} contra) =
[(t.meta, pretty "cannot apply non-function type" <+> line <+> prettyType a Open)]
prettyNotCheckSpine (Step2 (This contra)) = prettyNotChecks contra
prettyNotCheckSpine (Step2 (That contra)) = prettyNotCheckSpine contra
prettyNotCheckSpine (Step2 (Both contra1 contra2)) =
prettyNotChecks contra1 ++ prettyNotCheckSpine contra2
prettyAnyNotSynths (Step (This contra)) = prettyNotSynths contra
prettyAnyNotSynths (Step (That contra)) = prettyAnyNotSynths contra
prettyAnyNotSynths (Step (Both contra1 contra2)) =
prettyNotSynths contra1 ++ prettyAnyNotSynths contra2
prettyAnyNotChecks meta Base1 =
[(meta
, pretty "missing components" <+> line <+>
concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
)]
prettyAnyNotChecks meta (Step1 {t, l} contra) =
[(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
prettyAnyNotChecks meta (Step2 i (This contra)) =
case [| (nameOf i).value |] of
Val _ => prettyNotChecks contra
prettyAnyNotChecks meta (Step2 i (That contra)) = prettyAnyNotChecks meta contra
prettyAnyNotChecks meta (Step2 i (Both contra1 contra2)) =
case [| (nameOf i).value |] of
Val _ => prettyNotChecks contra1 ++ prettyAnyNotChecks meta contra2
prettyAnyNotBranches meta Base1 =
[(meta
, pretty "missing cases" <+> line <+>
concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
)]
prettyAnyNotBranches meta (Step1 {t, l} contra) =
[(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
prettyAnyNotBranches meta (Step2 i (This contra)) =
case [| (nameOf i).value |] of
Val _ => prettyNotChecks contra
prettyAnyNotBranches meta (Step2 i (That contra)) = prettyAnyNotBranches meta contra
prettyAnyNotBranches meta (Step2 i (Both contra1 contra2)) =
case [| (nameOf i).value |] of
Val _ => prettyNotChecks contra1 ++ prettyAnyNotBranches meta contra2
|
