Previously, promoteLetDecName would convert every DTyVarBndrSpec in an outermost forall to an invisible argument in a promoted type family equation. This is not quite right, however, as https://github.com/goldfirere/singletons/issues/585 reveals: we do not want to convert inferred type variable binders to invisible arguments.
To do this properly, we introduce a new tvbSpecsToBndrVis function, which converts a list of DTyVarBndrSpecs to a list of DTyVarBndrVises, dropping any DTyVarBndrSpecs with an InferredSpec in the process. We then use tvbSpecsToBndrVis in promoteLetDecName, which neatly fixes https://github.com/goldfirere/singletons/issues/585.
Previously,
promoteLetDecNamewould convert everyDTyVarBndrSpecin an outermostforallto an invisible argument in a promoted type family equation. This is not quite right, however, as https://github.com/goldfirere/singletons/issues/585 reveals: we do not want to convert inferred type variable binders to invisible arguments.To do this properly, we introduce a new
tvbSpecsToBndrVisfunction, which converts a list ofDTyVarBndrSpecs to a list ofDTyVarBndrVises, dropping anyDTyVarBndrSpecs with anInferredSpecin the process. We then usetvbSpecsToBndrVisinpromoteLetDecName, which neatly fixes https://github.com/goldfirere/singletons/issues/585.