Evaluating types and determining instantiability of an instance

[David Fox]

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 <jan.bracker at googlemail.com>
wrote:

> 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
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151105/58950e8b/attachment-0001.html>