`interpret` relies on the `Show` instance of `TypeRep`, which isn't right once kinds matter.

[ShapeOfMatter]

interpret relies on the Show instance of TypeRep, which doesn't yield syntactically valid expressions when it needs to specify the contextual kind of a polykinded constructor.

You can see a concrete example of the problem this causes on Stack Overflow.

It looks like this might be fixable by using Type.Reflection.... instead of Data.Typeable..... I'd be glad to try to help; we're right at the limits of my current understanding of Haskell.

Issue thread at Polysemy, for reference.

[ShapeOfMatter]

I set up a fork for trying to fix this. Here's the commit with what I've got so far:
https://github.com/ShapeOfMatter/hint/commit/9319cec1edeaaaba940e48f91f4d446f80984c4c

In effect, this strips out all kind specifications. It's not clear to me if that's ok.

The other two alternatives would be:

• Providing a kind specification for every type and type constructor. Under the hood this would involve a lot of parenthesis; I assume that's not actually a problem.
• Wrapping the whole type specification in a ((...) :: *) or some more descriptive alias of *.

Supposing either of those were necessary though, we may be out of luck. Kind Signatures are a language extension, and I assume we can't just activate an extension in the wrapped GHC... right?

[gelisam]

Thanks! I don't see the part which filters out the kind specifications; we definitely don't want to filter out all the type arguments which look like kinds, only the arguments which should be invisible. I assume that splitTyConApp simply doesn't return the invisible arguments?

[gelisam]

Kind Signatures are a language extension, and I assume we can't just activate an extension in the wrapped GHC... right?

hint allows the user to choose which language extensions they want to enable and disable. I would be fine with forcing KindSignatures to always be on, but I don't understand how that would help. The type already has kind * because it is type of a value, and since the invisible arguments are invisible, they can be inferred from the other arguments. So I think your proposed solution is the only one which works.

[ShapeOfMatter]

we definitely don't want to filter out all the type arguments which look like kinds, only the arguments which should be invisible.

I'm not sure what you mean by invisible arguments, or by type arguments which look like kinds, so I don't know if that could be a problem or not.

splitTyConApp gives us access to a TyCon instead of a TypeRep; this happens to leave out the kind signature. I'm pretty sure this could only ever matter if the type constructor in question were polykinded. I don't know if it matters when the constructor is polykinded.

The type already has kind * because it is type of a value

I haven't been able to think of any exceptions to this, but I don't want to trust my own knowledge.
It seems like an important detail that interpret only works on values of monomorphic types. Not knowing how that guarantee is enforced I can't say if the proposed change might undermine it.

Supposing all the above hand-wringing is over nothing, I would next add an appropriate unit/regression test and then open a pull request?

[gelisam]

I'm not sure what you mean by invisible arguments, or by type arguments which look like kinds, so I don't know if that could be a problem or not.

Consider these three types:

{-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-}
data Foo    a       deriving Typeable
data Bar   (a :: k) deriving Typeable
data Baz k (a :: k) deriving Typeable

Thanks to the PolyKinds extension, the a in Foo a has a polymorphic kind. We can make that explicit with KindSignatures, and that what I did with Bar (a :: k). Without PolyKinds, Foo a would be equivalent to Foo (a :: *) instead of Foo (a :: k).

GHC Haskell now supports dependent kinds, which is what makes Baz possible: the kind of a depends on the value of a previous type parameter, k. Comparing Bar and Baz, we can say that k is an invisible type parameter in Bar, but that it is visible in Baz, because the user must specify k when writing a Baz type, e.g. Baz Bool 'True, but must not specify k when writing a Bar type, e.g. Bar 'True. Even though the user does not specify k, it's still there as an invisible type parameter; when the user writes Bar 'True, ghc infers that the kind of 'True is Bool, and passes Bool as an invisible k argument to Bar.

Let's look at the Show output for the TypeReps of all these types.

λ> typeRep $ Proxy @(Foo 'True)
Foo Bool 'True

λ> typeRep $ Proxy @(Bar 'True)
Bar Bool 'True

λ> typeRep $ Proxy @(Baz Bool 'True)
Baz Bool 'True

The Show instance prints the invisible ks and the visible ks in the same way! That seems pretty confusing, but whatever, that's the syntax which the ghc team chose. We can't use Show, because we need to obtain the strings "Foo 'True", "Bar 'True" and "Baz Bool 'True", not the strings "Foo Bool 'True", "Bar Bool 'True" and "Baz Bool 'True". Thanks for spotting that bug by the way!

When you wrote "this strips out all kind specifications", I was worried that you were only looking at cases like Foo and Bar, and were forgetting about cases like Baz. Indeed, if you removed Bool everywhere, it would solve the problem for Foo and Bar, but would introduce a new problem for Baz, because Baz 'True is not valid either. That's why I said "we definitely don't want to filter out all the type arguments which look like kinds, only the arguments which should be invisible". We should only remove the Bool in the Foo and Bar cases, not in the Baz case.

Up to now I thought your splitTyConApp solution managed to distinguish between visible and invisible type arguments. Unfortunately, I've just tried it and it doesn't work for Baz:

λ> splitTyConApp $ typeRep $ Proxy @(Foo 'True)
(Foo,['True])

λ> splitTyConApp $ typeRep $ Proxy @(Bar 'True)
(Bar,['True])

λ> splitTyConApp $ typeRep $ Proxy @(Baz Bool 'True)
(Baz,['True])

So we need to keep searching for a proper solution! I haven't yet looked for a way to distinguish between visible and invisible type arguments, I don't know if it's even possible using Typeable's API. Thanks for your effort so far, and if you have more questions, don't hesitate to ask!

[gelisam]

It seems like an important detail that interpret only works on values of monomorphic types. Not knowing how that guarantee is enforced I can't say if the proposed change might undermine it.

To be honest, I don't know either! interpret was written before I joined the project.

[gelisam]

Supposing all the above hand-wringing is over nothing, I would next add an appropriate unit/regression test and then open a pull request?

Since you already wrote some code, I do think it would make more sense to discuss that code in a PR rather than an issue, as it would allow CI to run on your code and it would allow me to write review comments next to your code. We now know that your code is not quite correct yet, but it doesn't need to be perfect before sending it as a PR! Creating a PR is a perfectly good way to start a discussion. As is opening an issue; I'm not saying you should have opened a PR, I'm saying you can if you want :) Thanks again for contributing, this project deserves a lot more love than I currently give it!

[gelisam]

using ghci's :force command, I was able to inspect the internal representation of the TypeReps for the three types. Unfortunately, the (large) internal representation for all of those has the same shape, and differs only in a few numbers and internal pointers, many of which are different between runs. So I don't think TypeRep contains the information we need. We'll have to use the ghc API, and/or ask the ghc devs to improve Typeable's API.

[gelisam]

I reported it the the ghc team at https://gitlab.haskell.org//ghc/ghc/issues/14341#note_246287

[ShapeOfMatter]

Thank you! I'm following that thread, but it's looking less and less likely that I'll be able to help!

[gelisam]

I did some experiments with everything I could grab from Data.Typeable, Type.Reflection and Type.Reflection.Unsafe, and Foo, Bar and Baz all behave exactly the same. I suspect that invisible type parameters get desugared to visible type parameters at a phase which precedes the phase at which the TypeRep of each type gets constructed.

Where else might the visibility information be stored? GHC.Generics has metadata about the type, such as which package it comes from, but no information about the type variables:

λ> :kind! Rep (Foo 'True)
M1 D ('MetaData "Foo" "Ghci2" "interactive" 'False) V1
λ> :kind! Rep (Bar 'True)
M1 D ('MetaData "Bar" "Ghci3" "interactive" 'False) V1
λ> :kind! Rep (Baz Bool 'True)
M1 D ('MetaData "Baz" "Ghci4" "interactive" 'False) V1

TemplateHaskell's reify does list the type variables:

λ> reify ''Foo
TyConI (DataD [] Ghci2.Foo [KindedTV "a" () (VarT "k")] Nothing [] [])
()
λ> reify ''Bar
TyConI (DataD [] Ghci3.Bar [KindedTV "a" () (VarT "k")] Nothing [] [])
()
λ> reify ''Baz
TyConI (DataD [] Ghci4.Baz [KindedTV "k" () StarT,KindedTV "a" () (VarT "k")] Nothing [] [])
()

And so does :kind:

λ> :kind Foo
k -> *
λ> :kind Bar
k -> *
λ> :kind Baz
forall k -> k -> *

:kind seems particularly promising because forall k -> specifically means "visible". Also, since interpret is already invoking the ghc API to evaluate the code, it seems easier to invoke the ghc API in order to obtain the kind of a type than it would be to somehow trigger TemplateHaskell code to run.

[samuel-gelineau-at-well-dot]

Good news: while Data.Typeable.TypeRep's Show instance prints the invisible arguments, GHC.Type's Outputable instance doesn't. All which remains is to convert a TypeRep to a Type. But that's a bit tricky.

I can convert T1, T2, T3, Bool and 'True just fine, and I can use them to construct our three types as follow:

1. mkTyConApp T1 [Bool, 'True] is T1 'True
2. mkTyConApp T2 [Bool, 'True] is T2 'True
3. mkTyConApp T3 [Bool, 'True] is T3 Bool 'True

Since I do need to provide the Bool in all cases, I will need to figure out from the TypeRep that a Bool is expected there. But since splitTyConApp does not include the Bool argument, I need to get it from elsewhere. Where?