chore: don't check type of erased arguments in FixedParams analysis (#9602)

This commit is contained in:
Cameron Zwarich 2025-08-04 19:41:36 -07:00 committed by GitHub
parent 6e06978961
commit f236328bc3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -145,7 +145,7 @@ partial def evalApp (declName : Name) (args : Array Arg) : FixParamM Unit := do
have : i < main.params.size := h.2
let param := main.params[i]
let val ← evalArg args[i]
unless val == .val i || (val == .erased && param.type.isErased) do
unless val == .val i || val == .erased do
-- Found non fixed argument
-- Remark: if the argument is erased and the type of the parameter is erased we assume it is a fixed "propositonal" parameter.
modify fun s => { s with fixed := s.fixed.set! i false }