Constructor saturation fix
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
commit40ae2c944b89751d9c4ed88cbd9f1caaa4fa7738
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 1 Apr 2017, 01:14 (10 years ago)
parent2c001c9
src/Idris/DataOpts.hs+1−1
@@ -97,7 +97,7 @@ applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term
9797applyDataOptRT n tag arity uniq args
9898 | length args == arity = doOpts n args
9999 | 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)
101101 in bind extra tm
102102 where
103103 satArgs n = map (\i -> sMN i "sat") [1..n]