Normalisation of class methods during typechecking #48
Labels
Comments
ollef
added a commit
that referenced
this issue
Oct 31, 2017
This requires some changes to the normalisation machinery and to the elaborator. * The whnf function is now parameterised by how it should handle unsolved class constraints. When typechecking, this parameter is the class instance elaborator. * The class instance elaborator is now parameterised by what it should do with constraints it still didn't manage to solve. When normalising, we want to keep the constraints as the `UnsolvedConstraint` global, since it allows the type of the constraint to contain bound variables. When generalising, we want to (like before) make the constraints `Exist` metavars, such that they are picked up as free vars that can be generalised. Fixes #48.
ollef
added a commit
that referenced
this issue
Oct 31, 2017
This requires some changes to the normalisation machinery and to the elaborator. * The whnf function is now parameterised by how it should handle unsolved class constraints. When typechecking, this parameter is the class instance elaborator. * The class instance elaborator is now parameterised by what it should do with constraints it still didn't manage to solve. When normalising, we want to keep the constraints as the `UnsolvedConstraint` global, since it allows the type of the constraint to contain bound variables. When generalising, we want to (like before) make the constraints `Exist` metavars, such that they are picked up as free vars that can be generalised. Fixes #48. The elaboration during normalisation will not take into account local constraints (e.g. stemming from `MyClass a =>` constraints in a type signature), but I believe this is not necessary since those constraints are still unknown and will not reduce further anyway. So I think it's OK to leave those for the full elaboration pass. (I might be wrong though...)
ollef
added a commit
that referenced
this issue
Oct 31, 2017
This requires some changes to the normalisation machinery and to the elaborator. * The whnf function is now parameterised by how it should handle unsolved class constraints. When typechecking, this parameter is the class instance elaborator. * The class instance elaborator is now parameterised by what it should do with constraints it still didn't manage to solve. When normalising, we want to keep the constraints as the `UnsolvedConstraint` global, since it allows the type of the constraint to contain bound variables. When generalising, we want to (like before) make the constraints `Exist` metavars, such that they are picked up as free vars that can be generalised. Fixes #48. The elaboration during normalisation will not take into account local constraints (e.g. stemming from `MyClass a =>` constraints in a type signature), but I believe this is not necessary since those constraints are still unknown and will not reduce further anyway. So I think it's OK to leave those for the full elaboration pass. (I might be wrong though...)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Currently class instances are elaborated and filled in after the main typechecking has been done which means that we can't rely on them reducing to something while typechecking even if the instance is known. This is a desirable feature if we e.g. want to use methods that return types in a way that relies on the actual type of the instance.
To fix this we should interleave the class instance elaboration with the type checking. We will probably want the post-typechecking elaboration pass too though since unifications in distant parts of a function can affect the instances.
The text was updated successfully, but these errors were encountered: