Show instance for TypeReps is a bit broken

There are three problems.

1. Showing typereps of tuples can produce unnecessary parentheses:

   Prelude K T> typeRep @(Int, Maybe Bool)
   (Int,(Maybe Bool))

   The fix is trivial.

2. Showing typereps of ticked (i.e., lifted) tuples and lists gives hard-to-read results, because it does not use the usual special syntax:

   Prelude K T> typeRep @'(Int, Maybe Bool)
   '(,) * * Int (Maybe Bool)
   
   Prelude K T> typeRep @'[1,2,3]
   ': Nat 1 (': Nat 2 (': Nat 3 ('[] Nat)))

   Fixing the lifted tuple case is trivial. Fixing the lifted list case is slightly less trivial, but not hard.

3. Type operator applications are not shown infix.

   Prelude K T> typeRep @(Maybe :*: Either Int)
   :*: * Maybe (Either Int)

   This is the hardest problem to fix, although it's probably not too terribly hard. See ticket:14341#comment:143749 for thoughts.

changed weight to 5

added Tbug Trac import Typeable core libraries labels

Actually, there's a third problem as well: type operators are not shown infix! The solution, I believe, is to add operator precedence to TyCon, and then to use something akin to Show derivation machinery in showTypeRep. I imagine we don't need to worry too much about showing these things efficiently, at least for the foreseeable future. SomeTypeRep has no Read instance, so there's no substantial risk of anyone trying to use its Show instance for anything other than error messages and interactive exploration.

changed the description

There's also a problem with displaying partially applied tuple type constructors:

λ> typeRep @((,,))
()
λ> typeRep @((,,,,,,,) Int Word)
(Int,Word)

The problem seems to be that showTypeable doesn't check the arity of the constructor and just applies showArgs to the type arguments.

changed milestone to %8.6.1

I whipped up D5080 which solves the correctness problem mentioned in ticket:14341#comment:158724 simply.

Trac metadata

Trac field	Value
Differential revisions	D4084 → D4084, D5080

mentioned in commit 846fe904

There is still more than could be done here but at least the correctness issues are solved.

added Pnormal label

Another problem is that the Show output includes invisible type parameters, and as a result, the output is not a valid type. All but the first example from the description would be invalid if used in a Haskell program:

{-# LANGUAGE DataKinds, TypeOperators #-}
module Main where

import Data.Proxy
import GHC.Generics
import GHC.TypeLits


-- ok
ex1 :: (Int,(Maybe Bool))
ex1 = undefined

-- error:
-- Expected kind ‘* -> * -> k0’, but ‘ '(,) * *’ has kind ‘(*, *)’
ex2 :: Proxy ('(,) * * Int (Maybe Bool))
ex2 = undefined

ex2_fixed :: Proxy ('(,) Int (Maybe Bool))
ex2_fixed = undefined

-- error:
-- Operator applied to too few arguments: :
ex3 :: Proxy (': Nat 1 (': Nat 2 (': Nat 3 ('[] Nat))))
ex3 = undefined

-- error:
-- Expected kind ‘k1 -> k0’, but ‘ '(:) Nat 1’ has kind ‘[*]’
-- Expected kind ‘[*]’, but ‘1’ has kind ‘Nat’
-- Expected kind ‘k2 -> k1’, but ‘ '(:) Nat 2’ has kind ‘[*]’
-- Expected kind ‘[*]’, but ‘2’ has kind ‘Nat’
-- Expected kind ‘k4 -> k2’, but ‘ '(:) Nat 3’ has kind ‘[*]’
-- Expected kind ‘[*]’, but ‘3’ has kind ‘Nat’
-- Expected kind ‘* -> k1’, but ‘'[]’ has kind ‘[k0]’
ex3_partialFix :: Proxy ('(:) Nat 1 ('(:) Nat 2 ('(:) Nat 3 ('[] Nat))))
ex3_partialFix = undefined

ex3_fixed :: Proxy ('(:) 1 ('(:) 2 ('(:) 3 ('[]))))
ex3_fixed = undefined

-- error:
-- Operator applied to too few arguments: :*:
ex4 :: Proxy (:*: * Maybe (Either Int))
ex4 = undefined

-- error:
-- Expected kind ‘* -> *’, but ‘*’ has kind ‘*’
-- Expecting one more argument to ‘Either Int’
ex4_partialFix :: Proxy ((:*:) * Maybe (Either Int))
ex4_partialFix = undefined

ex4_fixed :: Proxy ((:*:) Maybe (Either Int))
ex4_fixed = undefined

While I would be happiest if TypeRep's Show instance could be fixed so that it always outputs a valid type, I'd be happy too if I could write my own TypeRep -> String function which does. Unfortunately, TypeRep's current API does not reveal which type parameters are visible and which are invisible.

SomeTypeRep has no Read instance, so there's no substantial risk of anyone trying to use its Show instance for anything other than error messages and interactive exploration.

The hint package uses TypeRep's Show output to generate some Haskell code of the form expr :: Type, which is then interpreted by the GHC API. I did not write that code, but I'm now maintaining it.

The fact that TypeRep's Show output is not a valid type causes a recently-reported bug in the hint package.

changed the description

First thought: oof, this will be annoying, because we need to annotate visibility at every application.

Second thought: but TypeRep doesn't support poly-kinded types, so really all we need is the info on TyCons. That's much easier.

Third thought: actually, even that's easy: all the trKindVars (that's a terrible field name; they're args, not vars) are invisible.

Fourth thought: oof, specificity.

So: we would need to add a list of specificities to GHC.Types.TyCon, and then use those when printing. Anything that's Inferred is just skipped; anything that's Specified gets printed with an @ prefix. Annoying is the fact that TcTypeable (I think) will have to be updated to produce the right TyCons now.

Is the Show instance for TypeRep supposed to produce a valid Haskell type? It seems a bit dubious to use it to generate Haskell code or for anything other than debugging.

It is already documented along those lines so an easier fix would be to beef up the documentation or remove the instance.

I think it's reasonable to hope for valid Haskell code. And we're relatively close to that ideal...

all the trKindVars (that's a terrible field name; they're args, not vars) are invisible.

Hmm, are they? Maybe I'm not using the word "invisible" correctly. In A syntax for visible dependent quantification, you gave the following example and said that k is "visible because every (fully-applied) use of T must pass in a value for k visibly (explicitly)".

data T k (a :: k)

I would thus contend that in the following type, k is invisible, because fully-applied uses of T2 must not pass in a value for k. That's the problem with TypeRep's Show instance: it passes in a value for k even though it shouldn't.

data T2 (a :: k)

I compiled ghc HEAD, made Data.Typeable.Internal public, and obtained the following, indicating that trKindVars contains the k argument (in this case Bool) whether k is visible or not.

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds, TypeApplications #-}
import Data.Typeable.Internal

data T k (a :: k)
data T2 (a :: k)

main :: IO ()
main = do
  let TrApp {trAppFun = t } = typeRep @(T Bool 'True)
  let TrApp {trAppFun = t2} = typeRep @(T2 'True)
  print (trTyCon t , trKindVars t)  -- (T,[Bool])
  print (trTyCon t2, trKindVars t)  -- (T2,[Bool])

Is the Show instance for TypeRep supposed to produce a valid Haskell type? It seems a bit dubious to use it to generate Haskell code or for anything other than debugging.

I agree that hint is assuming something of TypeRep's Show instance which isn't guaranteed by the documentation of TypeRep nor Show. In fact, our first course of action was to ignore the Show instance and to write our own function from TypeRep to String which does satisfy the guarantees we need it to satisfy. Unfortunately, the API in Data.Typeable does not provide the information I need in order to write such a function.

hint is already using the GHC API, so maybe there's a way for me to obtain the information I need in a different way? Is there a way to convert a TypeRep from base form into a Type from the GHC API?

Unfortunately, the API in Data.Typeable does not provide the information I need in order to write such a function.

What concretely is currently lacking? This sounds like something that should be addressed regardless of the Show instance issues.

You would need to know visibility information to get this right, and TypeRep currently doesn't store that. So it's not just an API change -- we need to change our data structures, all the way down to TyCon, to add this feature.

If you're using the GHC API, can you get compileExpr to return the Type and HValue rather than just the HValue?

It seems possible to modify hscParsedStmt in order to call exprType on the result of deSugarExpr which isn't very deep down the call stack from compileExpr.

I had forgotten about visible dependent quantification in that post. But, regardless, my fourth thought means we'd have to store specificities... really, we should store full visibilities (i.e. ArgFlags).

I don't think there's a way to go from TypeRep to Type.

@mpickering's suggestion sounds reasonable, but I have not looked at the details. I do think it would be a nice property to add to have Show TypeRep offer guarantees, but if we're not motivated by a concrete need, maybe it's not worth the effort.

My originating use-case was run-time evaluation of values in a customized Polysemy DLS. Whether or not this is useful or advisable is still unclear; I don't even have a POC yet.

I'd first tried to use the plugins library, but I ran into dependency problems in Cabal and got the impression that it wasn't being maintained. Going back and digging into its source code a little, it looks like it's heart is an OS process fork to call GHC, and then loading the (temporary) binary file into the current runtime using Data.Dynamic. My guess is that this isn't a superior approach.

On the other hand, I don't see any use in that stack of anything's Show instance. I'll see if I can apply the Data.Dynamic pattern to the relevant hint functions....