tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

Fix monomorphization bugs #66

Closed VictorCMiraldo closed 2 years ago

VictorCMiraldo commented 2 years ago

This PR extends monomorphization to handle all type arguments before the first term argument; we can now fully monomorphize:

const @Int @Bool x y

Which will replace the call site with const@Int@Bool and will produce a suitable definition. We can't fully monomorphize:

constWithWeirdArgs :: forall a . a -> forall b . -> b -> a

constWithWeirdArgs @Int x @Bool y

We will only monomoprhize the first type argument. It's unclear to me whether we want to produce a warning when we find definitions like constWithWeirdArgs above. Might be worthwhile for debugging purposes.

Additionally, this PR fixes important bugs in the computation of the types of monomorphized constructors and in the example parser.

serras commented 2 years ago

Which will replace the call site with const@Int@Bool and will produce a suitable definition. We can't fully monomorphize:

constWithWeirdArgs :: forall a . a -> forall b . -> b -> a

constWithWeirdArgs @Int x @Bool y

We will only monomoprhize the first type argument. It's unclear to me whether we want to produce a warning when we find definitions like constWithWeirdArgs above. Might be worthwhile for debugging purposes.

I am right now working on a prenexify transformation which pushes all the "big lambdas" to the front, which would allow us to handle every rank-1 function, even when "hidden" as in that type.