git.iko.soy/Idris-dev
on master help sign in
Constructor saturation fix
40ae2c9Edwin Brady
src/Idris/DataOpts.hs+1−1
compare with master
unifiedsplit
@@ -97,7 +97,7 @@ applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term
97applyDataOptRT n tag arity uniq args
97applyDataOptRT n tag arity uniq args
98 | length args == arity = doOpts n args
98 | length args == arity = doOpts n args
99 | otherwise = let extra = satArgs (arity - length args)
99 | otherwise = let extra = satArgs (arity - length args)
100− tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)
100+ tm = doOpts n (map (weakenTm (length extra)) args ++ map (\n -> P Bound n Erased) extra)
101 in bind extra tm
101 in bind extra tm
102 where
102 where
103 satArgs n = map (\i -> sMN i "sat") [1..n]
103 satArgs n = map (\i -> sMN i "sat") [1..n]