@@ -367,7 +367,7 @@ data InfoNote v loc
367
367
-- job to use the binding with the smallest containing scope so as to respect variable
368
368
-- shadowing.
369
369
-- This is used in the LSP.
370
- VarBinding v (Type v loc )
370
+ VarBinding v loc (Type v loc )
371
371
| -- | The usage of a particular variable. We report the variable and its location so we can match a given source location with a specific symbol later in the LSP.
372
372
VarMention v loc
373
373
deriving (Show )
@@ -394,7 +394,7 @@ substituteSolved ::
394
394
InfoNote v loc
395
395
substituteSolved ctx = \ case
396
396
(SolvedBlank b v t) -> SolvedBlank b v (applyCtx ctx t)
397
- VarBinding v t -> VarBinding v (applyCtx ctx t)
397
+ VarBinding v loc t -> VarBinding v loc (applyCtx ctx t)
398
398
i -> i
399
399
400
400
@@ -815,7 +815,7 @@ extend' e c@(Context ctx) = Context . (: ctx) . (e,) <$> i'
815
815
extend :: (Var v ) => Element v loc -> Context v loc -> M v loc (Context v loc )
816
816
extend e c = do
817
817
case e of
818
- Ann v _loc t -> noteVarBinding v t
818
+ Ann v loc t -> noteVarBinding v loc t
819
819
_ -> pure ()
820
820
either compilerCrash pure $ extend' e c
821
821
@@ -1122,8 +1122,8 @@ noteTopLevelType e binding typ = case binding of
1122
1122
-- | Take note of the types and locations of all bindings, including let bindings, letrec
1123
1123
-- bindings, lambda argument bindings and top-level bindings.
1124
1124
-- This information is used to provide information to the LSP after typechecking.
1125
- noteVarBinding :: (Var v ) => v -> Type v loc -> M v loc ()
1126
- noteVarBinding v t = btw $ VarBinding v t
1125
+ noteVarBinding :: (Var v ) => v -> loc -> Type v loc -> M v loc ()
1126
+ noteVarBinding v loc t = btw $ VarBinding v loc t
1127
1127
1128
1128
noteVarMention :: (Var v ) => v -> loc -> M v loc ()
1129
1129
noteVarMention v loc = do
@@ -1237,20 +1237,13 @@ synthesizeWanted (Term.Constructor' r) =
1237
1237
synthesizeWanted tm@ (Term. Request' r) =
1238
1238
fmap (wantRequest tm) . ungeneralize . Type. purifyArrows
1239
1239
=<< getEffectConstructorType r
1240
- synthesizeWanted tm @ (Term. Let1Top' top binding e) = do
1240
+ synthesizeWanted (Term. Let1Top' top binding boundVarAnn e) = do
1241
1241
(tbinding, wb) <- synthesizeBinding top binding
1242
1242
v' <- ABT. freshen e freshenVar
1243
1243
when (Var. isAction (ABT. variable e)) $
1244
1244
-- enforce that actions in a block have type ()
1245
1245
subtype tbinding (DDB. unitType (ABT. annotation binding))
1246
- case tm of
1247
- outer@ (ABT. Tm' (Term. Let _ rhs abs @ (ABT. Term _ _ (ABT. Abs v' body)))) -> do
1248
- -- let innerAnn = ABT.annotation inner
1249
- -- tbinding' = ABT.annotation binding
1250
- Debug. debugM Debug. Temp " synthesizeWanted (let binding)" (v', (" outer" :: Text , anythingToString $ ABT.annotation outer ), (" rhs" :: Text , anythingToString $ ABT.annotation rhs ), (" abs" :: Text , anythingToString $ ABT.annotation abs ), (" body" :: Text , anythingToString $ ABT.annotation body ))
1251
- _ -> pure ()
1252
- appendContext [Ann v' (error " Unset Ann loc: synthesizeWanted" ) tbinding]
1253
- -- Debug.debugM Debug.Temp "synthesizeWanted (missing annotation)" (v', anythingToString $ ABT.annotation tm, binding)
1246
+ appendContext [Ann v' boundVarAnn tbinding]
1254
1247
(t, w) <- synthesize (ABT. bindInheritAnnotation e (Term. var () v'))
1255
1248
t <- applyM t
1256
1249
when top $ noteTopLevelType e binding tbinding
@@ -1338,7 +1331,7 @@ synthesizeWanted e
1338
1331
1339
1332
-- ->I=> (Full Damas Milner rule)
1340
1333
-- | Term.Lam' body <- e = do
1341
- | tm @ (ABT. Tm' (Term. Lam (ABT. Abs' body))) <- e = do
1334
+ | (ABT. Tm' (Term. Lam (ABT. Abs' boundVarAnn body))) <- e = do
1342
1335
-- arya: are there more meaningful locations we could put into and
1343
1336
-- pull out of the abschain?)
1344
1337
[arg, i, e, o] <-
@@ -1351,14 +1344,8 @@ synthesizeWanted e
1351
1344
let it = existential' l B. Blank i
1352
1345
ot = existential' l B. Blank o
1353
1346
et = existential' l B. Blank e
1354
- case tm of
1355
- ABT. Term _ tmAnn (ABT. Tm (Term. Lam (ABT. Term _ absAnn (ABT. Abs v body)))) -> do
1356
- Debug. debugM Debug. Temp " Lambda binding anns" (v, anythingToString tmAnn, anythingToString absAnn, anythingToString $ ABT. annotation body)
1357
- _ -> pure ()
1358
- let annLoc = error " Unset Ann loc: synthesizeWanted"
1359
1347
appendContext $
1360
- [existential i, existential e, existential o, Ann arg annLoc it]
1361
- Debug. debugM Debug. Temp " tm arg loc (missing annotation)" arg
1348
+ [existential i, existential e, existential o, Ann arg boundVarAnn it]
1362
1349
1363
1350
when (Var. typeOf i == Var. Delay ) $ do
1364
1351
-- '(1 + 1) turns into a lambda with an arg variable of type Var.Delay
@@ -1689,7 +1676,6 @@ checkPattern scrutineeType p =
1689
1676
v <- getAdvance p
1690
1677
v' <- lift $ freshenVar v
1691
1678
lift . appendContext $ [Ann v' loc scrutineeType]
1692
- Debug. debugM Debug. Temp " Pattern binding anns" (v, anythingToString loc)
1693
1679
pure [(v, v')]
1694
1680
-- Ex: [42, y, Foo z]
1695
1681
Pattern. SequenceLiteral loc ps -> do
@@ -1777,7 +1763,6 @@ checkPattern scrutineeType p =
1777
1763
v <- getAdvance p
1778
1764
v' <- lift $ freshenVar v
1779
1765
lift . appendContext $ [Ann v' loc scrutineeType]
1780
- Debug. debugM Debug. Temp " As Pattern anns" (v, anythingToString loc)
1781
1766
((v, v') : ) <$> checkPattern scrutineeType p'
1782
1767
-- ex: { a } -> a
1783
1768
-- ex: { (x, 42) } -> a
@@ -1913,7 +1898,7 @@ annotateLetRecBindings isTop letrec =
1913
1898
pure (Term. ann (loc binding) e t2, t2, vloc)
1914
1899
-- If we're not using an annotation, we make one up. There's 2 cases:
1915
1900
1916
- lam@ (Term. Lam' _ ) ->
1901
+ lam@ (Term. Lam' {} ) ->
1917
1902
-- If `e` is a lambda of arity K, we immediately refine the
1918
1903
-- existential to `a1 ->{e1} a2 ... ->{eK} r`. This gives better
1919
1904
-- inference of the lambda's ability variables in conjunction with
@@ -2476,29 +2461,23 @@ checkWanted want m (Type.Forall' body) = do
2476
2461
ABT. bindInheritAnnotation body (universal' () x)
2477
2462
-- =>I
2478
2463
-- Lambdas are pure, so they add nothing to the wanted set
2479
- checkWanted want (Term. Lam' body) (Type. Arrow'' i es o) = do
2480
- let annLoc = error " checkWanted: missing annotation"
2464
+ checkWanted want (Term. Lam' boundVarAnn body) (Type. Arrow'' i es o) = do
2481
2465
x <- ABT. freshen body freshenVar
2482
2466
markThenRetract0 x $ do
2483
- Debug. debugM Debug. Temp " checkWanted:lam (missing annotation) " x
2484
- extendContext (Ann x annLoc i)
2467
+ Debug. debugM Debug. Temp " checkWanted:Lam " (x, anythingToString boundVarAnn)
2468
+ extendContext (Ann x boundVarAnn i)
2485
2469
body <- pure $ ABT. bindInheritAnnotation body (Term. var () x)
2486
2470
checkWithAbilities es body o
2487
2471
pure want
2488
- checkWanted want tm@ (Term. Let1Top' top binding m) t = do
2489
- case tm of
2490
- outer@ (ABT. Tm' (Term. Let _ rhs abs @ (ABT. Term _ _ (ABT. Abs v' body)))) -> do
2491
- Debug. debugM Debug. Temp " checkWanted:Let" (v', (" outer" :: Text , anythingToString $ ABT.annotation outer ), (" rhs" :: Text , anythingToString $ ABT.annotation rhs ), (" abs" :: Text , anythingToString $ ABT.annotation abs ), (" body" :: Text , anythingToString $ ABT.annotation body ))
2492
- _ -> pure ()
2493
- let annLoc = error " checkWanted: missing annotation"
2472
+ checkWanted want (Term. Let1Top' top binding boundVarAnn m) t = do
2494
2473
(tbinding, wbinding) <- synthesizeBinding top binding
2495
2474
want <- coalesceWanted wbinding want
2496
2475
v <- ABT. freshen m freshenVar
2497
2476
markThenRetractWanted v $ do
2498
2477
when (Var. isAction (ABT. variable m)) $
2499
2478
-- enforce that actions in a block have type ()
2500
2479
subtype tbinding (DDB. unitType (ABT. annotation binding))
2501
- extendContext (Ann v annLoc tbinding)
2480
+ extendContext (Ann v boundVarAnn tbinding)
2502
2481
checkWanted want (ABT. bindInheritAnnotation m (Term. var () v)) t
2503
2482
checkWanted want (Term. LetRecNamed' [] m) t =
2504
2483
checkWanted want m t
0 commit comments