Evaluating types and determining instantiability of an instance

[Richard Eisenberg]

On Nov 5, 2015, at 1:12 PM, Jan Bracker <jan.bracker at googlemail.com> wrote:
> 
> 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