Evaluating types and determining instantiability of an instance
Hello, I am trying to write a type checker plugin and I noticed that I keep trying to reimplement functionality that GHC type system already implements, but I can't seem to find a way to access the functionality. Part of these features I already asked in another (previous) email [1] to the mailing list and I am sorry if this will duplicate part of that discussion. 1. Is there a function in the type system which I can use to evaluate type functions and expand type synonyms (including associated instances)? Ideally I would want something that looks like this 'Type -> TcM Type'. I know that this kind of evaluation is not necessarily possible (e.g. type variables that can't be matched against in a type function application), but it would be helpful if the function could at least evaluate/expand as far as is possible in the current context. That way I don't have to manually lookup type family instances or type synonyms and make mistakes by doing so. This would also ease the support for the different type system extensions available, which I currently have to manually reimplement. 2. If I have an instance and a number of type arguments for that instance, is there an easy way to check if that instance is instantiated by those arguments? Something of the form '[Ct] -> ClsInst -> [Type] -> TcM (Maybe EvTerm)' would be useful. This function would take the given and derived constraints and deliver evidence for the instantiation if it is possible or return nothing if it is not. Again, if there are some open type variables I know this is not always possible in general and I am aware that this, in its full generality, requires a call to the constraint solver. But currently I am manually walking through the instance constraints to check if they are instantiated given the arguments [3] and then I also manually produce evidence [2]. In that process I ignore type equalities, type synonym and type families, because that would require me to implement question 1. I suspect this kind of functionality should exists somewhere within the GHC API. I would want this function to work with type arguments, whose only type variables already occur in the given and derived constraints. I think in that case it should always be possible to determine if the instance is instantiated. Best regards, Jan Bracker [1] https://mail.haskell.org/pipermail/ghc-devs/2015-November/010342.html [2] https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymon... [3] https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymon...
I think what you want is what I have attempted to do in th-context:
https://hackage.haskell.org/package/th-context
But it uses template-haskell types rather than GHC internal types.
On Thu, Nov 5, 2015 at 10:12 AM, Jan Bracker
Hello,
I am trying to write a type checker plugin and I noticed that I keep trying to reimplement functionality that GHC type system already implements, but I can't seem to find a way to access the functionality. Part of these features I already asked in another (previous) email [1] to the mailing list and I am sorry if this will duplicate part of that discussion.
1. Is there a function in the type system which I can use to evaluate type functions and expand type synonyms (including associated instances)? Ideally I would want something that looks like this 'Type -> TcM Type'. I know that this kind of evaluation is not necessarily possible (e.g. type variables that can't be matched against in a type function application), but it would be helpful if the function could at least evaluate/expand as far as is possible in the current context. That way I don't have to manually lookup type family instances or type synonyms and make mistakes by doing so. This would also ease the support for the different type system extensions available, which I currently have to manually reimplement.
2. If I have an instance and a number of type arguments for that instance, is there an easy way to check if that instance is instantiated by those arguments? Something of the form '[Ct] -> ClsInst -> [Type] -> TcM (Maybe EvTerm)' would be useful. This function would take the given and derived constraints and deliver evidence for the instantiation if it is possible or return nothing if it is not. Again, if there are some open type variables I know this is not always possible in general and I am aware that this, in its full generality, requires a call to the constraint solver. But currently I am manually walking through the instance constraints to check if they are instantiated given the arguments [3] and then I also manually produce evidence [2]. In that process I ignore type equalities, type synonym and type families, because that would require me to implement question 1. I suspect this kind of functionality should exists somewhere within the GHC API. I would want this function to work with type arguments, whose only type variables already occur in the given and derived constraints. I think in that case it should always be possible to determine if the instance is instantiated.
Best regards, Jan Bracker
[1] https://mail.haskell.org/pipermail/ghc-devs/2015-November/010342.html [2] https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymon... [3] https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymon...
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
On Nov 5, 2015, at 1:12 PM, Jan Bracker
1. Is there a function in the type system which I can use to evaluate type functions and expand type synonyms (including associated instances)? Ideally I would want something that looks like this 'Type -> TcM Type'. I know that this kind of evaluation is not necessarily possible (e.g. type variables that can't be matched against in a type function application), but it would be helpful if the function could at least evaluate/expand as far as is possible in the current context. That way I don't have to manually lookup type family instances or type synonyms and make mistakes by doing so. This would also ease the support for the different type system extensions available, which I currently have to manually reimplement.
I think FamInstEnv.normaliseType is the function you're looking for. You can get the FamInstEnvs argument from tcGetFamInstEnvs.
2. If I have an instance and a number of type arguments for that instance, is there an easy way to check if that instance is instantiated by those arguments? Something of the form '[Ct] -> ClsInst -> [Type] -> TcM (Maybe EvTerm)' would be useful. This function would take the given and derived constraints and deliver evidence for the instantiation if it is possible or return nothing if it is not. Again, if there are some open type variables I know this is not always possible in general and I am aware that this, in its full generality, requires a call to the constraint solver. But currently I am manually walking through the instance constraints to check if they are instantiated given the arguments [3] and then I also manually produce evidence [2]. In that process I ignore type equalities, type synonym and type families, because that would require me to implement question 1. I suspect this kind of functionality should exists somewhere within the GHC API. I would want this function to work with type arguments, whose only type variables already occur in the given and derived constraints. I think in that case it should always be possible to determine if the instance is instantiated.
I'm less familiar with this. Does InstEnv.lookupInstEnv do it for you? I hope this is helpful! Richard
participants (3)
-
David Fox -
Jan Bracker -
Richard Eisenberg