Skip to content

Commit

Permalink
Constructor saturation fix
Browse files Browse the repository at this point in the history
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 idris-lang#3713
  • Loading branch information
edwinb committed Apr 1, 2017
1 parent 2c001c9 commit 40ae2c9
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Idris/DataOpts.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down

0 comments on commit 40ae2c9

Please sign in to comment.