edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-02 09:47:22 +03:00
Code Issues Projects Releases Wiki Activity

Use expected type on adding laziness annotations

Browse Source 
This will be the correct one, since the annotations get us to the
expected type.
This commit is contained in:
Edwin Brady 2020-03-12 11:13:50 +00:00
parent fc9863b275
commit 20686425de
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/TTImp/Elab/Check.idr
View File

@ -555,7 +555,7 @@ convertWithLazy withLazy prec fc elabinfo env x y
_ => InTerm prec in
catch
(do let lazy = !isLazyActive && withLazy
logGlueNF 5 "Unifying" env x
logGlueNF 5 ("Unifying " ++ show withLazy) env x
logGlueNF 5 "....with" env y
vs <- if isFromTerm x && isFromTerm y
then do xtm <- getTerm x
@ -639,9 +639,9 @@ checkExpP rig prec elabinfo env fc tm got (Just exp)
dumpConstraints 5 False
case addLazy vs of
NoLazy => pure (ctm, got)
AddForce r => pure (TForce fc r tm, got)
AddForce r => pure (TForce fc r tm, exp)
AddDelay r => do ty <- getTerm got
pure (TDelay fc r ty tm, got)
pure (TDelay fc r ty tm, exp)
checkExpP rig prec elabinfo env fc tm got Nothing = pure (tm, got)
export