@@ -1158,22 +1158,26 @@ infer typer = loop
1158
1158
case Dhall.Map. lookup x xTs' of
1159
1159
Just _T' -> return _T'
1160
1160
Nothing -> die (MissingField x _E'')
1161
- _ -> do
1162
- let e' = eval values e
1163
-
1164
- let e'' = quote names e'
1165
-
1166
- case e' of
1167
- VUnion xTs' ->
1168
- case Dhall.Map. lookup x xTs' of
1169
- Just (Just _T') -> return (VHPi x _T' (\ _ -> e'))
1170
- Just Nothing -> return e'
1171
- Nothing -> die (MissingConstructor x e)
1172
-
1173
- _ -> do
1174
- let text = Dhall.Pretty.Internal. docToStrictText (Dhall.Pretty.Internal. prettyLabel x)
1175
-
1176
- die (CantAccess text e'' _E'')
1161
+ _ | VRecord xTs' <- eval values e ->
1162
+ case Dhall.Map. lookup x xTs' of
1163
+ Just _T' -> loop ctx (quote names _T')
1164
+ Nothing -> die (MissingField x _E'')
1165
+ | otherwise -> do
1166
+ let e' = eval values e
1167
+
1168
+ let e'' = quote names e'
1169
+
1170
+ case e' of
1171
+ VUnion xTs' ->
1172
+ case Dhall.Map. lookup x xTs' of
1173
+ Just (Just _T') -> return (VHPi x _T' (\ _ -> e'))
1174
+ Just Nothing -> return e'
1175
+ Nothing -> die (MissingConstructor x e)
1176
+
1177
+ _ -> do
1178
+ let text = Dhall.Pretty.Internal. docToStrictText (Dhall.Pretty.Internal. prettyLabel x)
1179
+
1180
+ die (CantAccess text e'' _E'')
1177
1181
Project e (Left xs) -> do
1178
1182
case duplicateElement xs of
1179
1183
Just x -> do
@@ -1185,6 +1189,9 @@ infer typer = loop
1185
1189
1186
1190
let _E'' = quote names _E'
1187
1191
1192
+ let text =
1193
+ Dhall.Pretty.Internal. docToStrictText (Dhall.Pretty.Internal. prettyLabels xs)
1194
+
1188
1195
case _E' of
1189
1196
VRecord xTs' -> do
1190
1197
let process x =
@@ -1196,11 +1203,25 @@ infer typer = loop
1196
1203
1197
1204
fmap adapt (traverse process xs)
1198
1205
1199
- _ -> do
1200
- let text =
1201
- Dhall.Pretty.Internal. docToStrictText (Dhall.Pretty.Internal. prettyLabels xs)
1206
+ _ | VRecord xTs' <- eval values e -> do
1207
+ let process x =
1208
+ case Dhall.Map. lookup x xTs' of
1209
+ Just _T' -> do
1210
+ _T'' <- loop ctx (quote names _T')
1211
+
1212
+ case _T'' of
1213
+ VConst c -> pure c
1214
+ _ -> die (CantProject text e _E'')
1215
+
1216
+ Nothing -> do
1217
+ die (MissingField x _E'')
1218
+
1219
+ cs <- traverse process xs
1220
+
1221
+ return (VConst (mconcat cs))
1202
1222
1203
- die (CantProject text e _E'')
1223
+ | otherwise -> do
1224
+ die (CantProject text e _E'')
1204
1225
1205
1226
Project e (Right s) -> do
1206
1227
_E' <- loop ctx e
0 commit comments