Evaluating types and determining instantiability of an instance

[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/Polymonad/Plugin/Evidence.hs#L29
[3]
https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymonad/Plugin/Instance.hs#L141
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151105/a8ddba05/attachment.html>