ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-11 08:55:23 +03:00
Code Issues Projects Releases Wiki Activity

Constructor saturation fix

Browse Source 
Constructors need to be saturated for compiling, but we need to be
careful if any existing arguments contain de Bruijn indices or we'll
break them when saturating. Fixes #3713
This commit is contained in:
Edwin Brady 2017-04-01 01:14:59 +01:00
parent 2c001c9bf1
commit 40ae2c944b
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/DataOpts.hs
View File

@ -97,7 +97,7 @@ applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term
applyDataOptRT n tag arity uniq args
| length args == arity = doOpts n args
| otherwise = let extra = satArgs (arity - length args)
tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)
tm = doOpts n (map (weakenTm (length extra)) args ++ map (\n -> P Bound n Erased) extra)
in bind extra tm
where
satArgs n = map (\i -> sMN i "sat") [1..n]