Skip to content

Commit 829cee8

Browse files
committed
[ fix ] Take only omega arguments into account when computing weight
1 parent c086bb7 commit 829cee8

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Deriving/DepTyCheck/Util/Reflection.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -858,7 +858,7 @@ getConsRecs = do
858858

859859
let wClauses = cons <&> \(con ** e) => do
860860
let wArgs = either (const empty) (fromMaybe empty . snd) e
861-
let lhsArgs : List (_, _) = mapI con.args $ \idx, arg => appArg arg <$> if contains idx wArgs
861+
let lhsArgs : List (_, _) = mapI con.args $ \idx, arg => appArg arg <$> if contains idx wArgs && arg.count == MW
862862
then let bindName = "arg^\{show idx}" in (Just bindName, bindVar bindName)
863863
else (Nothing, implicitTrue)
864864
let callSelfOn : Name -> TTImp

0 commit comments

Comments
 (0)