edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-27 18:53:42 +03:00
Code Issues Projects Releases Wiki Activity

Change multiplicity when inferring ->

Browse Source 
It should only be RigW if it wasn't known to be Rig0 already
This commit is contained in:
Edwin Brady 2020-02-02 15:51:49 +00:00
parent e5c70195da
commit 6cda854ceb
2 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Core/Unify.idr
View File

@ -370,9 +370,10 @@ instantiate {newvars} loc env mname mref mdef locs otm tm
updateLocsB : Binder (Term vs) -> Maybe (Binder (Term vs))
updateLocsB (Lam c p t) = Just (Lam c p !(updateLocs locs t))
updateLocsB (Let c v t) = Just (Let c !(updateLocs locs v) !(updateLocs locs t))
-- Make 'pi' binders have multiplicity W when we infer a metavariable,
-- Make 'pi' binders have multiplicity W when we infer a Rig1 metavariable,
-- since this is the most general thing to do if it's unknown.
updateLocsB (Pi c p t) = Just (Pi RigW p !(updateLocs locs t))
updateLocsB (Pi Rig1 p t) = Just (Pi RigW p !(updateLocs locs t))
updateLocsB (Pi c p t) = Just (Pi c p !(updateLocs locs t))
updateLocsB (PVar c p t) = Just (PVar c p !(updateLocs locs t))
updateLocsB (PLet c v t) = Just (PLet c !(updateLocs locs v) !(updateLocs locs t))
updateLocsB (PVTy c t) = Just (PVTy c !(updateLocs locs t))

2
src/TTImp/ProcessType.idr
View File

@ -119,7 +119,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
checkTerm idx InType (HolesOkay :: eopts) nest env
(IBindHere fc (PI Rig0) ty_raw)
(gType fc)
logTermNF 5 ("Type of " ++ show n) [] (abstractEnvType tfc env ty)
logTermNF 3 ("Type of " ++ show n) [] (abstractEnvType tfc env ty)
-- TODO: Check name visibility
def <- initDef n env ty opts