Don't generalise to RigW on let types

This is just as ugly as the similar hack for lambdas in 413d09da, but
necessary to allow let binding of linear functions.
This commit is contained in:
Edwin Brady 2020-02-11 17:54:11 +00:00
parent 666373e9db
commit 4ccddbac4a
3 changed files with 6 additions and 4 deletions

View File

@ -84,7 +84,6 @@ Information about external dependencies are presented in [INSTALL.md](INSTALL.md
Things still missing
====================
+ 'using' blocks
+ Disambiguation via 'with'
+ Cumulativity (so we currently have Type : Type! Bear that in mind when you
think you've proved something :))

View File

@ -174,7 +174,8 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty
-- try checking at Rig1 (meaning that we're using a linear variable
-- so the resulting binding should be linear)
(valv, valt, rigb) <- handle
(do c <- check (rigMult rigl rigc) elabinfo
(do c <- check (rigMult rigl rigc)
(record { preciseInf = True } elabinfo)
nest env nVal (Just (gnf env tyv))
pure (fst c, snd c, rigMult rigl rigc))
(\err => case err of

View File

@ -349,10 +349,12 @@ record ElabInfo where
implicitMode : BindMode
topLevel : Bool
bindingVars : Bool
preciseInf : Bool -- are types inferred precisely (True) or do we generalise
-- pi bindings to RigW (False, default)
export
initElabInfo : ElabMode -> ElabInfo
initElabInfo m = MkElabInfo m NONE False True
initElabInfo m = MkElabInfo m NONE False True False
export
tryError : {vars : _} ->
@ -631,4 +633,4 @@ checkExp : {vars : _} ->
(term : Term vars) ->
(got : Glued vars) -> (expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
checkExp rig = checkExpP rig False
checkExp rig elabinfo = checkExpP rig (preciseInf elabinfo) elabinfo