Rework derivation of type representations for wired-in things
ClosedPublic

Authored by bgamari on Jan 13 2016, 5:10 PM.

Details

Summary

This is a work in progress.

Previously types defined by GHC.Types and GHC.Prim had their Typeable
representations manually defined in GHC.Typeable.Internals. This was
terrible, resulting in a great deal of boilerplate and a number of bugs
due to missing or inconsistent representations (see Trac #11120).

Here we take a different tack, initially proposed by Richard Eisenberg: We
wire-in the Module, TrName, and TyCon types, allowing them to be used in
GHC.Types. We then allow the usual type representation
generation logic to handle this module.

GHC.Prim, on the other hand, is a bit tricky as it has no object code of its own.
To handle this we instead place the type representations for the types defined
here in GHC.Types.

On the whole this eliminates several special-cases as well as a fair amount
of boilerplate from hand-written representations. Moreover, we get full
coverage of primitive types for free.

Test Plan

Validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
bgamari updated this revision to Diff 6182.Jan 13 2016, 5:10 PM
bgamari retitled this revision from to [WIP] Rework derivation of type representations for wired-in things.
bgamari updated this object.
bgamari edited the test plan for this revision. (Show Details)
bgamari updated the Trac tickets for this revision.
bgamari updated this revision to Diff 6186.Jan 14 2016, 7:24 AM
bgamari edited edge metadata.

Things are beginning to take shape

bgamari updated this object.Jan 14 2016, 3:55 PM
bgamari edited edge metadata.
bgamari updated this revision to Diff 6198.Jan 14 2016, 3:57 PM
  • Rework
  • Nearly done? nope
bgamari updated this revision to Diff 6265.Jan 18 2016, 8:56 AM
bgamari edited edge metadata.

A different approach

bgamari updated this revision to Diff 6275.Jan 18 2016, 12:57 PM
bgamari edited edge metadata.

Getting very close now

bgamari updated this revision to Diff 6276.Jan 18 2016, 1:22 PM
bgamari edited edge metadata.

Inching closer

bgamari updated this revision to Diff 6277.Jan 18 2016, 2:33 PM
bgamari edited edge metadata.

It compiles

bgamari added subscribers: simonpj, goldfire.

How does this look?

Unfortunately it appears that this didn't fix the rather peculiar output from the TypeOf test from my previous attempt at fixing this (e782e882ba455c671cb35751053822a74a9f66b7), where the representation of TYPE is bizarrely history dependent.

For instance, consider

import Data.Typeable
import GHC.Types
main = do
    print $ typeOf (Proxy :: Proxy TYPE)
    print $ typeOf (Proxy :: Proxy (Int Eq))
    print $ typeOf (Proxy :: Proxy TYPE)
    print $ typeOf (Proxy :: Proxy Eq)

This produces,

Proxy (Levity -> *) TYPE
Proxy * (Eq Int)
Proxy (Levity -> *) TYPE
Proxy (* -> *) Eq

If we comment out the first print we instead get,

Proxy Constraint (Eq Int)
Proxy (Levity -> Constraint) TYPE
Proxy (Constraint -> Constraint) Eq

Moreover, I've realized that I have no idea how we would handle things like typeOf (Proxy :: Proxy Char#). Currently this fails with,

>>> typeOf (Proxy :: Proxy Char#)

<interactive>:11:18: error:
    • Illegal unlifted type: Char#
    • In an expression type signature: Proxy Char#
      In the first argument of ‘typeOf’, namely ‘(Proxy :: Proxy Char#)’
      In the expression: typeOf (Proxy :: Proxy Char#)

It seems that properly supporting this would be rather tricky with the current limitations of TypeInType given that this would call for a Typeable Char# constraint yet even with -XTypeInType -XPolyKinds -XKindSignatures -XMagicHash,

>>> class Hi (a :: TYPE l) where hi :: Proxy a -> String
>>> instance Hi Char# where hi Proxy = "hi"

<interactive>:10:10: error:
    • Illegal unlifted type: Char#
    • In the instance declaration for ‘Hi Char#’

but perhaps I am missing something here.

At this point, I suspect addressing Trac #11120 completely may be beyond the scope of 8.0. Instead we should just retain the existing "illegal unlifted type" and make sure that it covers unlifted types found in promoted constructors' kinds so that programs like

data CharHash = CharHash Char#
main = print $ typeOf (Proxy :: Proxy 'CharHash)

don't fail with a compiler panic as they do currently.

Nevertheless, I believe the refactoring done in this diff may still be a worthwhile endeavor. It replaces a fair amount of fragile handwritten boilerplate with a much more consistent mechanism for producing type representations.

bgamari updated this revision to Diff 6279.Jan 18 2016, 4:06 PM
bgamari edited edge metadata.

Rebase

bgamari retitled this revision from [WIP] Rework derivation of type representations for wired-in things to Rework derivation of type representations for wired-in things.Jan 18 2016, 4:06 PM
bgamari edited edge metadata.
bgamari updated this object.
goldfire edited edge metadata.Jan 18 2016, 4:50 PM

Why does Proxy :: Proxy Char# fail? It shouldn't.

I mean, I know there's code in TcValidity to rule this out. But I think that's too aggressive. But maybe not to be fixed today.

Why does Proxy :: Proxy Char# fail? It shouldn't.

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.1.20160118
$ ghci
GHCi, version 8.1.20160118: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ben/.ghci
λ> :set -XTypeInType -XMagicHash
λ> import GHC.Types
λ> import Data.Proxy
λ> :ty Proxy :: Proxy Char#

<interactive>:1:10: error:
    • Illegal unlifted type: Char#
    • In an expression type signature: Proxy Char#
      In the expression: Proxy :: Proxy Char#

I mean, I know there's code in TcValidity to rule this out. But I think that's too aggressive. But maybe not to be fixed today.

I'm all for loosening the restriction if this is sound. What cases in particular do you think should be allowed?

Anything that's well-kinded should be allowed, I think. We absolutely can't have #-kinded type parameters to datatypes. That should be checked for at datatype definition. But if we have a polykinded parameter to a datatype, I don't see the harm in letting it have kind #. Similarly, I think type family parameters of kind # should be OK (but are currently prohibited). But I do think this is all a larger question that doesn't need to be answered for 8.0.

Anything that's well-kinded should be allowed, I think. We absolutely can't have #-kinded type parameters to datatypes. That should be checked for at datatype definition. But if we have a polykinded parameter to a datatype, I don't see the harm in letting it have kind #. Similarly, I think type family parameters of kind # should be OK (but are currently prohibited). But I do think this is all a larger question that doesn't need to be answered for 8.0.

Fair enough; that does, however, leave us with the question of what to do about Trac #11120. My suggestion was to tighten up the check a bit farther to ensure that Proxy :: Proxy 'CharHash doesn't instill a sense of panic in the compiler.

I'm a bit lost. What's the problem here? Is it just that you can't test finding representations of unlifted types, because of the unlifted-type-check? None of the recent volley of comments should affect generation of the representations -- just the ability to query for them. If you query for them by means of a promoted data constructor, that would seem to be sufficient for testing.

Or is there something else going on?

bgamari updated this revision to Diff 6312.Jan 20 2016, 5:42 AM
bgamari edited edge metadata.
  • Unify mkPrelTyConRepName and mkWiredInTyConRepName
simonpj edited edge metadata.Jan 20 2016, 6:04 AM

See my comments on Trac Trac #11120

I'm a bit lost. What's the problem here? Is it just that you can't test finding representations of unlifted types, because of the unlifted-type-check?

Ahh yes, you are right. All is well. I confused myself.

bgamari added a comment.EditedJan 20 2016, 7:06 AM

The proof is in the pudding,

λ> :set  -XDataKinds -XTypeInType -XMagicHash
λ> import Data.Typeable
λ> import GHC.Exts
λ> typeRep (Proxy :: Proxy 'GHC.Exts.C#)
'C#
bgamari updated this object.Jan 20 2016, 7:12 AM
bgamari edited edge metadata.

Ok fine. Land it! Do please elaborate the Grand plan with a few more comments about any exceptions.

I thought you were removing defns from Data.Typeable.Internals, in favour of machine-generated ones? I can's see that here. And if doing that, might be able to put in GHC.Types after all

compiler/typecheck/TcTypeable.hs
139

Big Note here please! Or refer to up the "Grand plan" note, and say more there.

Ok fine. Land it!

Will do.

Do please elaborate the Grand plan with a few more comments about any exceptions.

They are already all mentioned; there is only one: representations for types in GHC.Prim get plopped in GHC.Types. Everything else is handled by the usual path.

Nevertheless, I'll have one read-through and elaborate where necessary.

I thought you were removing defns from Data.Typeable.Internals, in favour of machine-generated ones? I can's see that here. And if doing that, might be able to put in GHC.Types after all

Indeed this is what I do; try searching the diff for tc'True.

bgamari updated this revision to Diff 6313.Jan 20 2016, 7:49 AM
  • Add test for Trac #11120
  • A note
  • Eliminate user-writable rep names
bgamari updated this revision to Diff 6314.Jan 20 2016, 9:03 AM
bgamari edited edge metadata.
  • Add more comments
This revision was automatically updated to reflect the committed changes.