Opened 3 years ago

Closed 3 years ago

Last modified 13 months ago

#9858 closed bug (fixed)

Typeable instances should be kind-aware

Reported by: dreixel Owned by:
Priority: highest Milestone: 7.10.2
Component: Compiler Version: 7.9
Keywords: Cc: ecrockett0@…, int-e, oerjan, shachaf, lelf, dfeuer, liyang, ryan.gl.scott@…, dterei
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T9858a,b,c; should_run/T9858b
Blocked By: Blocking:
Related Tickets: #10000 Differential Rev(s): Phab:D652, Phab:D757
Wiki Page:

Description (last modified by bgamari)

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE AutoDeriveTypeable     #-}

import Data.Typeable

data A = A

main = print $ typeRep (Proxy :: Proxy A) == typeRep (Proxy :: Proxy 'A)

This returns True, but it should return False.

Change History (120)

comment:1 Changed 3 years ago by dreixel

Owner: set to dreixel

comment:2 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:3 Changed 3 years ago by crockeea

Cc: ecrockett0@… added

comment:4 Changed 3 years ago by int-e

This bug means that lambdabot cannot enable DataKinds (see #10000 for how to implement unsafeCoerce using this.)

I would really like to see this fixed in 7.10.1.

comment:5 Changed 3 years ago by int-e

One way of fixing this would be to prepend a prime (or some other non-capital letter character) to name_fs in TcGenDeriv.gen_Typeable_binds if the given tycon::TyCon is a promoted data constructur.

Is this sufficient or are there other ways in which having distinct type constructors with identical tyConName could cause the compiler to go wrong?

comment:6 Changed 3 years ago by int-e

Cc: int-e added
Milestone: 7.12.17.10.1
Priority: normalhigh

comment:7 in reply to:  5 ; Changed 3 years ago by dreixel

Replying to int-e:

One way of fixing this would be to prepend a prime (or some other non-capital letter character) to name_fs in TcGenDeriv.gen_Typeable_binds if the given tycon::TyCon is a promoted data constructur.

Is this sufficient (...)

I believe so. It should be a really simple fix.

comment:8 Changed 3 years ago by simonpj

Pedro when do you think you might get to this? Thanks

See also #10000

Simon

comment:9 in reply to:  7 ; Changed 3 years ago by oerjan

Replying to dreixel:

Replying to int-e:

One way of fixing this would be to prepend a prime (or some other non-capital letter character) to name_fs in TcGenDeriv.gen_Typeable_binds if the given tycon::TyCon is a promoted data constructur.

Is this sufficient (...)

I believe so. It should be a really simple fix.

Nope, here is a version based simply on using different promoted kinds (that are not visible in the Typeable instance). Also works to modify Shachaf's unsafeCoerce from #10000.

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE AutoDeriveTypeable     #-}

import Data.Typeable

data A t = A

main = print $ typeRep (Proxy :: Proxy (A :: Bool -> *))
               == typeRep (Proxy :: Proxy (A :: Ordering -> *))

comment:10 Changed 3 years ago by oerjan

Cc: oerjan added

comment:11 Changed 3 years ago by oerjan

For what it's worth, they don't have to be promoted kinds, * and * -> * also work.

Last edited 3 years ago by oerjan (previous) (diff)

comment:12 in reply to:  9 ; Changed 3 years ago by dreixel

Replying to oerjan:

Replying to dreixel:

Replying to int-e:

One way of fixing this would be to prepend a prime (or some other non-capital letter character) to name_fs in TcGenDeriv.gen_Typeable_binds if the given tycon::TyCon is a promoted data constructur.

Is this sufficient (...)

I believe so. It should be a really simple fix.

Nope, here is a version based simply on using different promoted kinds (that are not visible in the Typeable instance). Also works to modify Shachaf's unsafeCoerce from #10000.

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE AutoDeriveTypeable     #-}

import Data.Typeable

data A t = A

main = print $ typeRep (Proxy :: Proxy (A :: Bool -> *))
               == typeRep (Proxy :: Proxy (A :: Ordering -> *))

I think this example highlights a different limitation of Typeable, along the lines of #7897.

comment:13 in reply to:  12 Changed 3 years ago by oerjan

Replying to dreixel:

I think this example highlights a different limitation of Typeable, along the lines of #7897.

But #7897 doesn't break Safe Haskell like these examples do. And I think there is a common feature of the ones here: Typeable breaks because a typerep doesn't include the kind of the type.

comment:14 Changed 3 years ago by simonpj

Pedro: how do you suggest we proceed with this? It seems quite urgent if you can use it to write unsafeCoerce.

Simon

comment:15 Changed 3 years ago by shachaf

Cc: shachaf added

comment:16 in reply to:  14 Changed 3 years ago by oerjan

Replying to simonpj:

Pedro: how do you suggest we proceed with this? It seems quite urgent if you can use it to write unsafeCoerce.

Simon

If I may comment too, I think the long-term solution for these bugs cannot be anything less than including kind information in typereps, at least for type constructors of polymorphic kind.

However that may be too hard to get done in the short term, in which case one possibility might be to somehow disallow PolyKinds, or possibly Typeable instances for polykinds, in Safe Haskell. Note that exploiting this doesn't require any explicit extensions mentioning kinds, Typeable or deriving, this was my last version (works in GHCi 7.8.3):

{-# LANGUAGE TypeFamilies #-}

import Data.Typeable

type E = (:~:)

data family F p a b

newtype instance F a b (Proxy (Proxy :: * -> *)) = ID (a -> a)
newtype instance F a b (Proxy (Proxy :: (* -> *) -> *)) = UC (a -> b)

-- Needed to prevent faulty inlining in GHCi.  Maybe expand further if it
-- breaks at higher optimization levels.
munge = id

ecast :: E p q -> f p -> f q
ecast Refl = id

supercast ::
       F a b (Proxy (Proxy :: * -> *))
    -> F a b (Proxy (Proxy :: (* -> *) -> *))
supercast = case cast e of
    Just e' -> munge ecast e'
  where
    e = Refl
    e :: E (Proxy (Proxy :: * -> *)) (Proxy (Proxy :: * -> *))

uc :: a -> b
uc = case supercast (ID id) of UC f -> f

comment:17 Changed 3 years ago by thoughtpolice

Priority: highhighest

comment:18 Changed 3 years ago by dreixel

Here's the current definition of TypeRep:

data TypeRep = TypeRep {-# UNPACK #-} !Fingerprint TyCon [TypeRep]

data TyCon = TyCon {
   tyConHash    :: {-# UNPACK #-} !Fingerprint,
   tyConPackage :: String,
   tyConModule  :: String,
   tyConName    :: String
 }

Could we perhaps add a tyConKind :: TypeRep to TyCon, and make sure that it is used when computing the hash?

comment:19 Changed 3 years ago by goldfire

I see two different issues at work here:

  1. If we have data A = A, then (typeRep (Proxy :: Proxy A)) and (typeRep (Proxy :: Proxy 'A)) are equal. This is not a problem with kinds, but a problem with namespaces. To me, the salient difference between A and 'A is not that their kinds are different, but that they represent totally different entities. Fixing this issue is simple, either by adding some namespace information to TyCon or putting some marker in the tyConName string.
  1. If we have data B x (no constructors), then B :: forall k. k -> *. The types (B :: Bool -> *) and (B :: Ordering -> *) are actually, in Core, B Bool and B Ordering -- in Core, kind arguments are explicit. Thus, the TypeRep for B :: Bool -> * could feasibly be TypeRep <fingerprint> <B's TyCon> [<Bool's TypeRep>]. The change here isn't to the structure of TyCon, but instead mandating that all kind arguments are explicit in TypeReps, just like they are in Core. Indeed, it surprises me that this isn't already the case! I believe that making kind arguments explicit in TypeReps will be a simplification.

Personally, it seems adding kind information to TypeRep is not the best approach here.

comment:20 Changed 3 years ago by simonpj

Summary: Typeable instance for datatype and its promoted constructor is the sameTypeable instances should be kind-aware

Richard is spot on.

For (1), really A and 'A are entirely different, and should not compare as equal. That is probably easy to fix, by changing the fingerprint we generate for 'A.

For (2), yes absolultely, just as Maybe Int and Maybe Bool should have non-equal TypeReps, so should B 'Ordering and B 'Bool. The fact that is's a kind application isn't important. The reason that bug (2) happens is, I think, that the Typeable instance of B is generated by an instance declaration:

instance Typeable B where
  typeRep# _ = ...the TyCon for B....

This instance declaration is treated as source code, and source code does implicit kind instantiation. So we actually get

dfun :: forall k. Typeable (B k)
dfun = /\k. MkTypeableDict (...TyCon for B....)

We don't want this! Instead we want to treat (B 'Bool) just like Maybe Bool, using the application instance (in Data.Typeable.Internals), which looks roughly like this:

instance (Typeable s, Typeable a) => Typeable (s a) where
         -- See Note [The apparent incoherence of Typable]
  typeRep# _ = typeRep a `mkAppTy` typeRep b

We would like this to be done for kind applications as well as type applications.

So we need two changes

  • For type constructors, we need an instance that truly matches on B not on B k
  • We need to decompose kind applications as we do type applications.

To me it seems clear that we should move to treating Typeable more like we treat Coercible, i.e. as a built-in type class that the constraint solver knows how to solve, rather than as something handed with source-level instance declarations.

That would imply:

  • There would be no Typeable instances in the instance environment (which itself would be a modest saving).
  • Either
    1. every data type constructor automatically has a Typeable instance (which I favour), or
    2. we'd need a tiresome separate mechanism (a flag in the TyCon) to say whether it does or does not have a Typeable instance.

Note that this path might ultimately allow us to have a TypeRep for a polymorphic type, which we can't do right now.

What do people feel about (1) vs (2)? Why would we ever want a type not to be Typeable? Note that the code-size overhead is modest: a single top-level definition of a record defining the TyCon.

comment:21 Changed 3 years ago by goldfire

I vote for Simon's option 1 -- just make runtime type identification a feature of GHC Haskell, exposed through the Typeable interface. This will take a small amount of work to engineer, but I think the end state will be simpler than what we have now, and likely more efficient.

I will point out one drawback: I believe users will be confused about the need for Typeable constraints. After all, if every type is Typeable, then why include the constraint? We cognoscenti know that the Typeable constraint is just implicitly passing the runtime witness, but we'll have to be careful to explain this to those who think that class constraints are all about logical statements, not implicit type-determined parameters.

comment:22 in reply to:  21 Changed 3 years ago by crockeea

Replying to goldfire:

I will point out one drawback: I believe users will be confused about the need for Typeable constraints. After all, if every type is Typeable, then why include the constraint? We cognoscenti know that the Typeable constraint is just implicitly passing the runtime witness, but we'll have to be careful to explain this to those who think that class constraints are all about logical statements, not implicit type-determined parameters.

After using Haskell for several years, that still trips me up. If you are able to make everything Typeable, might there be a way to make the Typeable constraint implicit, at least when it's needed?

comment:23 Changed 3 years ago by Ptharien's Flame

If I may interject from the outside (so to speak), I think the best way to explain Simon's proposition (1) is in terms of parametricity, in a manner akin to the widely-expounded-upon use of monadic effects in Haskell. Adding a Typeable constraint is just like surrounding a type with IO: it allows more operations, while simultaneously marking the code as not-quite-pure in a specific way.

comment:24 Changed 3 years ago by simonpj

Folks, we need an interim solution for 7.10. A full fix sounds as if it'll take a little longer. But I'm anxious about releasing 7.10 with the ability to write unsafeCoerce in Safe Haskell.

One drastic remedy: do not derive Typeable for polykinded type constructors. That would be easy to implement, and would certainly fix it. But it's a bit drastic.

Any other offers? We need to do this in the next two weeks.

Better still would be to fix it properly of course.

Simon

comment:25 in reply to:  24 ; Changed 3 years ago by dreixel

Replying to simonpj:

One drastic remedy: do not derive Typeable for polykinded type constructors. That would be easy to implement, and would certainly fix it. But it's a bit drastic.

Isn't that very drastic? So a data constructor that is declared with PolyKinds on, but can be used without it (such as Proxy), won't be allowed to have a Typeable instance at all? Or would we allow a (orphan) Typeable instance to be derived in a module that does not have PolyKinds on? Even if so, I'm afraid this might have important ramifications, also given that SYB requires Typeable...

How about just marking Typeable instances for polykinded type constructors as Unsafe (if that's possible)?

comment:26 in reply to:  25 ; Changed 3 years ago by int-e

Replying to dreixel:

How about just marking Typeable instances for polykinded type constructors as Unsafe (if that's possible)?

Given how notoriously hard it is to control exports of instances, that won't be enough. To make things worse, the offending instance used here (for Proxy) is derived in Data.Typeable.Internal, which is marked Trustworthy. So conscientious users of safe Haskell would not be able to trust the base package anymore, rendering safe Haskell all but useless.

I guess the right way to leverage safe Haskell is to mark Data.Typeable as unsafe, and explain the situation in a big comment. It would still be a pain to track uses of Data.Typeable in Trustworthy modules of other libraries (say, lens and its dependencies).

I'm afraid there is no good interim solution here. I favor spj's suggestion, but #9111 suggests that some people actually use Typeable for Proxy.

comment:27 Changed 3 years ago by crockeea

To echo @dreixel: What exactly *is* SPJ's suggestion? Is it to not *automatically* derive Typeable instances for poly-kinded type constructors, or is to disallow standalone-derived instances as well?

comment:28 in reply to:  27 Changed 3 years ago by oerjan

Replying to crockeea:

To echo @dreixel: What exactly *is* SPJ's suggestion? Is it to not *automatically* derive Typeable instances for poly-kinded type constructors, or is to disallow standalone-derived instances as well?

Presumably it would be safe to allow a *single* standalone derivation in the same module that defines the type, as long as it's of actual monomorphic kind. That way, at least Proxy could still have a * -> * instance, which might be the one that is used the most in practice?

comment:29 Changed 3 years ago by oerjan

In fact, a single automatically derived instance (presumably defaulting as much as possible to *) should also be safe.

comment:30 Changed 3 years ago by simonpj

Yes, SPJ's drastic suggestion is: a polykinded type constructor cannot be an instance of Typeable, by deriving, or AutoDeriveTypable, or standalone deriving. Period. How bad would that be?

Here's an alternative proposal.

  • ....deriving( Typeable ) (and AutoDeriveTypeable) on a polykinded tycon will fail (with a helpful message)
  • But instead you can give any number of mono-kinded standalone instances
    deriving instance Typeable (Proxy :: (* -> *) -> *)
    

Comments on the alternative proposal

  • It's still not ideal because you can never declare "enough" instances and if you declare an extra one at some use site, it might conflict with someone else's.
  • It requires some modification to GHC, which current rejects such standalone deriving instances, precisely because they are not fully polymorphic.
  • And the kinds would have to be included in the fingerprint of the TyCon generated by the standalone derived instance.

But that seems ok as a holding position.

The "right" solution is, I think, at the bottom of comment:20. But NB that solution will mean that all these standalone derived instances would become illegal, so there is a backward compatibility cost. The drastic solution does not have this problem.

Last edited 3 years ago by simonpj (previous) (diff)

comment:31 Changed 3 years ago by simonpj

comment:32 in reply to:  30 Changed 3 years ago by oerjan

Replying to simonpj:

  • And the kinds would have to be included in the fingerprint of the TyCon generated by the standalone derived instance.

Once you have the mechanism for getting a kind representation to put in the fingerprint, how much harder is it to just make it work polymorphically while you're at it?

I'm not a GHC developer by any means, but I still had the hunch that this could be a main stumbling block to getting the proper solution working.

The "right" solution is, I think, at the bottom of comment:20. But NB that solution will mean that all these standalone derived instances would become illegal, so there is a backward compatibility cost. The drastic solution does not have this problem.

If *all* types later become Typeable automatically, then wouldn't it be safe and backward compatible to just ignore the explicit instances with a redundancy warning?

(I've occasionally been thinking that multiple derived instances for the same type and class should often be safely compatible with each other. If made by the same mechanism, they're guaranteed to have the same code, after all. Although I guess standalone deriving with explicit restricted type signature could complicate that.)

comment:33 in reply to:  19 ; Changed 3 years ago by oerjan

I see in the wiki page that the idea of putting kind arguments in TypeReps is hitting severe type system problems. I had another idea, which I didn't bother to bring up before since goldfire's idea looked much prettier. And now that I tried actually writing up a proof of concept, it looks even more monstrous :/

But anyway, here it is, sort of working, but with some obvious drawbacks:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Proxy

newtype TTypeRep a = TT String deriving Show
newtype KKindRep a = KK String deriving Show

class Kindable' (a :: k -> *) where
    kindRep :: KKindRep a

class Kindable' (Proxy :: k -> *) => Typeable' (a :: k) where
    typeRep :: TTypeRep a
    
instance Kindable' (Proxy :: * -> *) where
    kindRep = KK "*"

instance (Kindable' (Proxy :: k1 -> *), Kindable' (Proxy :: k2 -> *)) => Kindable' (Proxy :: (k1 -> k2) -> *) where
    kindRep = KK $ '(' : k1 ++ " -> " ++ k2 ++ ")"
      where
        KK k1 = kindRep :: KKindRep (Proxy :: k1 -> *)
        KK k2 = kindRep :: KKindRep (Proxy :: k2 -> *)

instance Kindable' (Proxy :: k -> *) => Typeable' (Proxy :: k -> *) where
    typeRep = TT $ "Proxy :: " ++ k
      where
        KK k = kindRep :: KKindRep (Proxy :: (k -> *) -> *)

main = do
    print (kindRep :: KKindRep (Proxy :: (* -> * -> *) -> *))
    print (typeRep :: TTypeRep (Proxy :: (* -> * -> *) -> *))
    print (kindRep :: KKindRep (Proxy :: ((* -> *) -> *) -> *))
    print (typeRep :: TTypeRep (Proxy :: ((* -> *) -> *) -> *))

comment:34 in reply to:  33 ; Changed 3 years ago by int-e

Replying to oerjan:

But anyway, here it is, sort of working, but with some obvious drawbacks:

One such drawback is that the Kindable' constraint is sort of infectious. One can using a type family for mapping kinds to types, which seems to overcome that particular shortcoming:

type family KindRep (p :: k)

data Star deriving Typeable
type instance KindRep (Proxy :: * -> *) = Star
type instance KindRep (Proxy :: (k -> k') -> *) = KindRep (Proxy :: k -> *) -> KindRep (Proxy :: k' -> *)

-- some data kinds: () and []
type instance KindRep (Proxy :: () -> *) = ()
type instance KindRep (Proxy :: [k] -> *) = [KindRep (Proxy :: k -> *)]

One could then have

instance Typeable (KindRep (Proxy :: k -> *)) => Typeable' (Proxy :: k -> *)

Here's some working code: http://lpaste.net/4263409010180358144

comment:35 Changed 3 years ago by lelf

Cc: lelf added

comment:36 Changed 3 years ago by dfeuer

Cc: dfeuer added

comment:37 Changed 3 years ago by ekmett

As a data point, disabling Typeable for polykinded code would actually break production code for me in a ways I don't see how to fix.

Code out there just switched from manual deriving of these instances pre 7.8 for a few particular cases, to the derived ones for 7.8+, but if you take away the derived instances and don't let folks write them by hand that case falls into a gap, where there is now no way to get even back to the 7.6 level of support.

comment:38 in reply to:  34 Changed 3 years ago by oerjan

Replying to int-e:

One such drawback is that the Kindable' constraint is sort of infectious. One can using a type family for mapping kinds to types, which seems to overcome that particular shortcoming:

This is already better, but also:

Wouldn't this type family become redundant if we had Richard's identification of types and kinds? Assuming this also means you can have classes with only kind parameters, you could possibly get rid of the need for all the Proxys and UndecidableInstances as well?

At which point this starts to seem a lot prettier.

Since I didn't give much comments in my previous version, the main ideas were:

  1. Including the kind of a type in its TTypeRep already at construction may not have the typing problems that the wiki page describes for a "polymorphic typerep" with separately applied kindrep arguments.
  2. You can construct representations for kinds already in current GHC code, although there's boilerplate because you cannot use kinds as "naked" parameters.

comment:39 in reply to:  30 Changed 3 years ago by dfeuer

Replying to simonpj:

The "right" solution is, I think, at the bottom of comment:20. But NB that solution will mean that all these standalone derived instances would become illegal, so there is a backward compatibility cost. The drastic solution does not have this problem.

Wouldn't it be (sufficiently) correct to simply ignore all Typeable instance declarations (deriving, standalone deriving, and otherwise), issuing a warning to that effect, instead of rejecting them outright?

comment:40 in reply to:  26 Changed 3 years ago by int-e

Replying to int-e:

I'm afraid there is no good interim solution here. I favor spj's suggestion, but #9111 suggests that some people actually use Typeable for Proxy.

I've changed my mind about SPJ's idea. It's very late in the ghc-7.10 release cycle, and the design of the long-term solution is still in flux, so any drastic stop-gap measure bears a significant risk of breaking users' code twice. And there are quite a lot of users, not least because Typeable is poly-kinded (see also Edward's comment:37 which carries some weight).

I'd rather see this bug documented and communicated prominently so that everybody who runs untrusted Haskell code knows about it, and take further measures to sandbox that code. (This is a good idea anyway; ghc, its RTS and the libraries are really too big to be trusted even with SafeHaskell enabled.)

comment:41 Changed 3 years ago by int-e

SPJ started a discussion about delaying the ghc-7.10 release for this here: https://www.haskell.org/pipermail/ghc-devs/2015-January/008189.html

comment:42 Changed 3 years ago by goldfire

Take a look at this wiki page. It includes a solution (the "medium-term solution") that we think can be done in time for 7.10 if there is a delay. What's nice about this one is that it should break no existing code. Depending on design decisions, we would probably warn about Typeable instances (which would no longer be necessary), but nothing should outright break.

Last edited 3 years ago by goldfire (previous) (diff)

comment:43 in reply to:  42 ; Changed 3 years ago by oerjan

Replying to goldfire:

What's nice about this one is that it should break no existing code.

It may be too weird to count as "existing code", but can it handle this?

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DeriveDataTypeable #-}

import Data.Typeable

newtype C a b = C () deriving Typeable

step :: Proxy (a :: k) -> Proxy (C a :: k -> *)
step Proxy = Proxy

nest :: Typeable a => Int -> Proxy a -> TypeRep
nest 0 x = typeRep x
nest n x = nest (n-1) (step x)

main = print $ nest 10 (Proxy :: Proxy ())

comment:44 Changed 3 years ago by liyang

Cc: liyang added

comment:45 in reply to:  43 ; Changed 3 years ago by goldfire

Replying to oerjan:

It may be too weird to count as "existing code", but can it handle this?

Let's see.

Everything is peachy until the second clause for nest. There, we assume Typeable <k> a (writing the implicit kind argument in angle brackets) and must produce Typeable <k -> *> (C <k> <k> a). I believe a sufficiently smart solver should be able to do this without difficulty. It will have access to fingerprint information for k, and should be able to build a fingerprint for k -> * from what it has. Good test case, but it seems workable with the proposed fix.

comment:46 Changed 3 years ago by oerjan

Ah, I had misunderstood what the wiki page said, then. Now this gives me an idea for an expanded test case.

If my picture of how such a solver would work is now more correct, then I think by expanding the kinds in my example a bit, we can get a case where the solver would need not just to build new kind reps, but also to take the kind rep inside its provided Typeable instance further apart. And for good measure let's include a data kind as well:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE AutoDeriveTypeable #-}

import Data.Typeable

newtype C a b = C ()

step :: Proxy (a :: [k] -> *) -> Proxy (C a :: [k -> *] -> *)
step Proxy = Proxy

nest :: Typeable (a :: [k] -> *) => Int -> Proxy a -> TypeRep
nest 0 x = typeRep x
nest n x = nest (n-1) (step x)

main = print $ nest 10 (Proxy :: Proxy (C () :: [()] -> *))

Assuming you would want to support this kind of code.

Last edited 3 years ago by oerjan (previous) (diff)

comment:47 in reply to:  46 Changed 3 years ago by goldfire

Here, we would be given Typeable <[k] -> *> a and need to derive Typeable <[k -> *] -> *> (C <[k] -> *> <[k -> *]> a). Yes, that would require decomposition, indicating that we should store more than just the kind fingerprint. Another very nice test case. Thanks!

comment:48 Changed 3 years ago by oerjan

I was going to say that this need to do kind decomposition when inferring Typeable instances is why this cannot be done just with standalone instances, and you need a solver.

In fact the last time I gave up on my attempt to express this in source code, it was because I realized that the fundamental instance

instance (Typeable a, Typeable b) => Typeable (a b)

already needs such decomposition to be written.

But today I had an epiphany: This can be expressed with current types, although with the annoying need to wrap kinds in proxies:

-- Ideally k itself should be the class argument, but that is not yet
-- supported.  I think this is what makes UndecidableInstances
-- necessary for defining instances.  Fortunately the instances seem to be
-- usable without it.
class (KindableParts a, a ~ Proxy) => Kindable (a :: k -> *) where
    type KindableParts a :: Constraint
    kindRep :: KindRep a

class Kindable (Proxy :: k -> *) => Typeable (a :: k) where
    typeRep :: proxy a -> TypeRep

I wrote up enough of a mock implementation to make the last test case above work with this. The code is a bit long, so I put it on my website.

comment:49 Changed 3 years ago by int-e

I'm wondering about the ramifications of this claim from Typeable#Medium-termsolution:

Although it is impossible to create all necessary Typeable instances for poly-kinded constructors at the definition site (there's an infinite number), it is possible to create Typeable "instances" on demand at use sites.

Consider the following function:

f = \(p :: Proxy Proxy) -> typeRep p

Because the kind information of the p argument is not fully known at the site of definition, I surmise that the corresponding Kindable (to use oerjan's nomenclature) constraint gets propagated outward, meaning that at the core language level, f gets an extra argument for passing the Kindable evidence for the unknown kind argument of the second Proxy type constructor.

It is my understanding that for the sake of backward compatibility, this argument is implicit and not visible (even as a constraint) in the Haskell-level type. Is that correct? I feel uncomfortable about this; I like to be able to see in the Haskell type of functions what kind of runtime evidence needs to be passed to a function to make it work. (In a slogan: hiding evidence is bad.)

The second thing I'm wondering about is what happens when polymorphic kinds are never instantiated at all. Is the following program valid, and if so, what will the kind of the Proxy be at runtime?

{-# LANGUAGE PolyKinds, DataKinds #-}
import Data.Typeable

main :: IO ()
main = print (typeRep (Proxy :: Proxy Proxy))
Last edited 3 years ago by int-e (previous) (diff)

comment:50 in reply to:  49 Changed 3 years ago by int-e

Replying to int-e:

f = \(p :: Proxy Proxy) -> typeRep p

Note that currently, the function has type Proxy Proxy -> Typeable. What will the type be under the proposed medium term solution? If we want full backward compatibility (and I personally don't think we should strive for that for examples like this one) then passing hidden extra evidence is the only way to go.

comment:51 in reply to:  49 ; Changed 3 years ago by goldfire

f = \(p :: Proxy Proxy) -> typeRep p

More fun test cases!

Let's see what GHC will do. First, we must insert kind unification variables:

Proxy :: forall (k :: BOX). k -> *
typeRep :: forall (k :: BOX) (proxy :: k -> *) (a :: k).
           Typeable <k> a => proxy a -> TypeRep

f = \(p :: Proxy <k0 -> *> (Proxy <k0>)) ->
    typeRep <k0 -> *> <Proxy <k0 -> *>> <Proxy <k0>> <$dict> p
  where
    $dict :: Typeable <k0 -> *> (Proxy <k0>)

We find that k0 isn't affected by any equality constraints, and so it can be generalized over. We can also generalize over the Typeable constraint:

f :: forall (k :: BOX). Typeable <k -> *> (Proxy <k>) => Proxy <k -> *> (Proxy <k>) -> TypeRep

In surface syntax, this looks like

f :: Typeable (Proxy :: k -> *) => Proxy (Proxy :: k -> *) -> TypeRep

Looks fine to me. Am I missing something? I agree that the solver can't decompose the Proxy <k> argument, but that should be OK. Finding Typeable instances (or Kindable instances) doesn't involve search, so GHC can look for the "Kindable" without decomposing first. If the Kindable isn't there, no decomposition.

comment:52 in reply to:  51 Changed 3 years ago by int-e

f :: Typeable (Proxy :: k -> *) => Proxy (Proxy :: k -> *) -> TypeRep

Looks fine to me. Am I missing something?

I'm happy with this type, it's very reasonable, and reflects the fact that some evidence (for Typeable) has to be provided by the caller.

My main point was that this change will not be 100% backwards compatible (note that the new inferred type for f is different from what ghc 7.10 RC2 infers.) I was also slightly afraid that you might want to fudge things (by omitting the extra evidence from Haskell-level type signatures) to make the medium term solution fully backward compatible, but apparently that fear was unjustified.

The open question is whether this incompatibility will affect existing real world code.

comment:53 in reply to:  51 Changed 3 years ago by oerjan

I agree with int-e that this might break some code, like his

main = print (typeRep (Proxy :: Proxy Proxy))

The problem is that in the old system, the Typeable instance is inferred with no need to consider the kind at all, so it becomes completely known at compile time. In the new system there will be an ambiguity. If my test with my mock implementation is any guide, GHC currently (well, 7.8.3) refuses to resolve such ambiguities.

As I suggested in private, a case like the above might be fixed backwards-compatibly by making kinds in need of unavailable Kindable evidence default to * in a very similar way to numerical defaulting. I suspect that if a user isn't providing an explicit kind signature that is the most likely result they want anyway.

comment:54 Changed 3 years ago by int-e

Here is another testcase, geared towards motivating kind-level Typeable evidence (also known as Kindable):

f :: Proxy (a :: k) -> Proxy (b :: k) -> Proxy (Proxy :: k -> *)
f _ _ = Proxy

g pa pb = typeRep (f pa pb)

If we allow kind-level Typeable constraints, i.e., Typeable (k :: BOX), we would have

g :: Typeable k => Proxy (a :: k) -> Proxy (b :: k) -> TypeRep

With just the type-level Typeable, we can choose between two constraints,

g :: Typeable (Proxy (a :: k)) => Proxy (a :: k) -> Proxy (b :: k) -> TypeRep
g :: Typeable (Proxy (b :: k)) => Proxy (a :: k) -> Proxy (b :: k) -> TypeRep

so which one should type inference prefer? Or would g require a type signature?

comment:55 Changed 3 years ago by goldfire

We are certainly not aiming for 100% backward compatibility. Indeed we can't -- unsafeCoerce compiles today, and we don't want it to compile tomorrow. So, at least that program will be omitted. Because of the conservative nature of type systems, some more programs will be excluded, most likely. We want this extra set to be small, but I'm not overly worried about it.

As for this example:

f :: Proxy (a :: k) -> Proxy (b :: k) -> Proxy (Proxy :: k -> *)
f _ _ = Proxy

g pa pb = typeRep (f pa pb)

I get

g (pa :: Proxy <k0> a0) (pb :: Proxy <k1> b0)
  = typeRep <(k2 -> *) -> *> <Proxy <(k2 -> *) -> *>> <Proxy <k2 -> *>> <$dict>
            (f <k2> <a1> <b1> pa pb)
  where
    $dict :: Typeable <(k2 -> *) -> *> (Proxy <k2 -> *>)

Unifying some variables and generalizing gives us

g <k :: BOX> <a :: k> <b :: k> (pa :: Proxy (a :: k)) (pb :: Proxy (b :: k))
  = typeRep <(k -> *) -> *> <Proxy <(k -> *) -> *>> <Proxy <k -> *>> <$dict>
            (f <k> <a> <b> pa pb)
  where
    $dict :: Typeable <(k -> *) -> *> (Proxy <k -> *>)

We then generalize over the Typeable constraint, giving

g :: forall (k :: BOX) (a :: k) (b :: k).
     Typeable <(k -> *) -> *> (Proxy <k -> *>)
  => Proxy <k> a -> Proxy <k> b -> TypeRep

or, in source Haskell

g :: Typeable (Proxy :: (k -> *) -> *)
  => Proxy (a :: k) -> Proxy (b :: k) -> TypeRep

Again, I don't see the ambiguity, and I think GHC would be able to infer this type without trouble... I don't see how this is a special case, really.

comment:56 in reply to:  55 Changed 3 years ago by int-e

Replying to goldfire:

g :: Typeable (Proxy :: (k -> *) -> *)
  => Proxy (a :: k) -> Proxy (b :: k) -> TypeRep

Again, I don't see the ambiguity, and I think GHC would be able to infer this type without trouble... I don't see how this is a special case, really.

You're right, it isn't.

comment:57 in reply to:  55 Changed 3 years ago by oerjan

Replying to goldfire:

Again, I don't see the ambiguity, and I think GHC would be able to infer this type without trouble... I don't see how this is a special case, really.

With that example, I've mostly been convinced that constraints separating out kinds aren't necessary.

I still think it would help backwards compatibility if kinds in Typeable contexts defaulted to * in situations exactly analogous to when types with numerical contexts do.

Once again, int-e's test case is illustrative:

main :: IO ()
main = print (typeRep (Proxy :: Proxy Proxy))

As far as I understand, without the type signature a solver would infer a type of

main :: Typeable (Proxy :: k -> *) => IO ()

and by defaulting k to * the code would still work, and probably do what was originally intended. Without defaulting it seems to me that it cannot work either with or without a signature.

comment:58 Changed 3 years ago by goldfire

This defaulting to * is precisely what happens without PolyKinds on. So anyone not worried about kind variables won't need to.

But I don't like this defaulting behavior if PolyKinds is on. If a user has specified PolyKinds and writes the code in comment:57, I would want an error to be reported. The choice of the kind variable here is potentially relevant to the programmer's desired behavior, and I think silently guessing a value is wrong here.

comment:59 in reply to:  58 Changed 3 years ago by oerjan

Replying to goldfire:

This defaulting to * is precisely what happens without PolyKinds on. So anyone not worried about kind variables won't need to.

Oh, so it is, on second testing. My first test (with my mock implementation, whose inferred types I think are "close enough" for the purpose) failed, but I only removed PolyKinds and must have left some other extension that implied it.

But I don't like this defaulting behavior if PolyKinds is on. If a user has specified PolyKinds and writes the code in comment:57, I would want an error to be reported. The choice of the kind variable here is potentially relevant to the programmer's desired behavior, and I think silently guessing a value is wrong here.

Good point, although I'm still wondering which option will break the least code...

comment:60 Changed 3 years ago by goldfire

I think your plan (of more defaulting to *) would break less code, but I think that someone saying Proxy Proxy without thinking about kinds yet specifying PolyKinds has made a mistake. After all, the goal is to make the TypeRep for Proxy :: * -> * and Proxy :: Bool -> * different. We should expect the user to specify which one they want.

comment:61 Changed 3 years ago by Austin Seipp <austin@…>

In b359c886cd7578ed083bcedcea05d315ecaeeb54/ghc:

Custom `Typeable` solver, that keeps track of kinds.

Summary:
This implements the new `Typeable` solver: when GHC sees `Typeable` constraints
it solves them on the spot.

The current implementation creates `TyCon` representations on the spot.

Pro: No overhead at all in code that does not use `Typeable`
Cons: Code that uses `Typeable` may create multipe `TyCon` represntations.

We have discussed an implementation where representations of `TyCons` are
computed once, in the module, where a datatype is declared.  This would
lead to more code being generated:  for a promotable datatype we need to
generate `2 + number_of_data_cons` type-constructro representations,
and we have to do that for all programs, even ones that do not intend to
use typeable.

I added code to emit warning whenevar `deriving Typeable` is encountered---
the idea being that this is not needed anymore, and shold be fixed.

Also, we allow `instance Typeable T` in .hs-boot files, but they result
in a warning, and are ignored.  This last one was to avoid breaking exisitng
code, and should become an error, eventually.

Test Plan:
1. GHC can compile itself.
2. I compiled a number of large libraries, including `lens`.
    - I had to make some small changes:
      `unordered-containers` uses internals of `TypeReps`, so I had to do a 1 line fix
    - `lens` needed one instance changed, due to a poly-kinded `Typeble` instance

3. I also run some code that uses `syb` to traverse a largish datastrucutre.
I didn't notice any signifiant performance difference between the 7.8.3 version,
and this implementation.

Reviewers: simonpj, simonmar, austin, hvr

Reviewed By: austin, hvr

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D652

GHC Trac Issues: #9858

comment:62 Changed 3 years ago by thoughtpolice

Status: newmerge

comment:63 Changed 3 years ago by Herbert Valerio Riedel <hvr@…>

In 47b5b5c2b2c92ba091313c36489588edadceaa9d/ghc:

base: drop redundant Typeable derivings

Thanks to #9858 `Typeable` doesn't need to be explicitly derived anymore.
This also makes `AutoDeriveTypeable` redundant, as well as some imports of
`Typeable` (removal of whose may be beneficial to #9707). This commit
removes several such now redundant use-sites in `base`.

Reviewed By: austin, ekmett

Differential Revision: https://phabricator.haskell.org/D712

comment:64 Changed 3 years ago by rwbarton

Owner: dreixel deleted
Status: mergenew

(Reopening for discussion)

Sorry for getting here a bit late; but I have some concerns about this change as it stands currently.

Abstractly my main concern is that we've made a change (implicitly deriving Typeable everywhere) for the wrong reasons, and concretely my main fear, given the timing of this change, is that we'll find the new approach is untenable for some reason or other and be forced back into a world in which explicit deriving Typeable is required.

I'm certainly not trying to say that implicitly deriving Typeable is the wrong decision; but it seems that it arose as fallout from the issue in this ticket and #10000 for technical reasons, and not because we decided that we really want it. We will always be able to transition to implicit deriving Typeable in the future, but transitioning back to explicit deriving Typeable loses compatibility with programs written for an earlier version of the compiler that had implicit deriving Typeable.

So, seeing as we are in the RC phase for 7.10, my recommendation would be:

  • Keep the requirement to explicitly derive Typeable (and keep AutoDeriveTypeable, etc.) as in 7.10 RC 2
  • Don't actually generate evidence terms when deriving Typeable. Instead mark the type as "Typeable-allowed".
  • When generating evidence in the Typeable solver, check that all of the types involved are marked as "Typeable-allowed".

comment:65 Changed 3 years ago by goldfire

To clarify comment:64, I understand that this proposal doesn't really change the recent patch under the hood, but just the user interface to it. (Yes, tracking Typeable-allowed-ness takes some under-the-hood work.) Please correct me if I'm wrong.

I think that having Typeable available for every type is the right thing to do. It's something I have wanted for some time. This ticket just made the change happen now instead of soon.

All that said, I can understand the worry that we'll paint ourselves into a corner here. It might be reasonable to adopt the proposal above for 7.10 and then relax it for 7.12, when we have more time to see possible strange interactions.

comment:66 in reply to:  64 Changed 3 years ago by hvr

Replying to rwbarton:

Abstractly my main concern is that we've made a change (implicitly deriving Typeable everywhere) for the wrong reasons, and concretely my main fear, given the timing of this change, is that we'll find the new approach is untenable for some reason or other and be forced back into a world in which explicit deriving Typeable is required.

Does artificially keeping require to explicitly derive Typeable during the 7.10 cycle actually help us identifying issues, rather than just releasing this into the wild with 7.10 and gather real-world data during 7.10's life-cycle?

Fwiw, IIRC we wanted to turn on AutoDeriveTypeable by default anyway sooner or later. So this change just accomplishes that by a different mechanism, but the outcome is the same IMO.

comment:67 Changed 3 years ago by simonpj

It's certainly possible to make it possible not to have Typeable. But it's a significant chunk of extra work, and at the moment we pretty strongly believe we'll want to throw it away anyway. I don't think we have a single example of a situation which having Typeable is bad.

However, if (against all the evidence) someone eventually produces a situation in which we don't want Typeable for some type, we can I suppose implement NoAutoDeriveTypable. So I don't think we are painting ourselves into any corners.

Reasonable questions, but I think we should proceed as planned.

Simon

comment:68 Changed 3 years ago by rwbarton

I'm not particularly concerned about the possibility of this change breaking any existing program; that seems rather unlikely. What I am concerned about is the possibility of another bug like #10000 being discovered that forces us to abandon this "all types are Typeable" approach.

It just seems like common sense to me to make large language changes like this at the start of a version's development, not one week before the last release candidate. (And I say large because there are probably tens of thousands of "deriving Typeable" out there. Yes I'd like to get rid of them too, but only if I could be reasonably sure that they won't have to be added back in for 7.10.2!)

comment:69 Changed 3 years ago by simonpj

Well I can't deny that it's possible. But if it happens, we can fix it, as I outline above. I'd just rather avoid investing effort that we expect to be useless.

comment:70 Changed 3 years ago by rwbarton

In that case perhaps we should advertise the new automatic Typeable deriving behavior as experimental in 7.10, so that users can decide whether they want to rely on it or not.

Also, I think it's definitely correct that (as it is currently) warn-deriving-typeable not be enabled by -Wall. We can turn on the warning in 7.12.

By the way, we may want to use a similar mechanism of generating evidence at the call site to handle #9557. For that problem, we would certainly need to track whether or not the class was derived at the definition site. So, I don't actually expect the effort to be useless. But the timing may be wrong here, unfortunately.

comment:71 Changed 3 years ago by thoughtpolice

Merged to ghc-7.10 (via 6f46fe15af397d448438c6b93babcdd68dd78df8).

comment:72 Changed 3 years ago by thoughtpolice

Differential Rev(s): Phab:D652
Milestone: 7.10.17.12.1
Priority: highestnormal

(In light of the merge for the immediate fixes, I'm demoting this bug and pushing it to 7.12.1, in case the discussion wants to continue. Simon has also indicated he wants to continue working on this area and redo some things, so we can leave this ticket open for that.)

comment:73 Changed 3 years ago by shachaf

This doesn't seem to be completely fixed:

λ> type A = (() :: *)
λ> type B = (() :: Constraint)
λ> typeRep (Proxy :: Proxy A) == typeRep (Proxy :: Proxy B)
True
λ> typeRep (Proxy :: Proxy (Proxy A)) == typeRep (Proxy :: Proxy (Proxy B))
False

Though I can't think of a way to write unsafeCoerce in this case.

comment:74 Changed 3 years ago by goldfire

You've hit smack into a blind spot of a dark corner of GHC's type system: * and Constraint are actually considered interchangeable in Core. So this failure isn't terribly surprising. But it's indeed a bug. I don't think it should be too hard to fix.

comment:75 Changed 3 years ago by oerjan

I also thought of that core thing but I doubt that's it... it seems to me that it's just two more entities that don't have different TypeCons, like in the original report of this ticket, and which don't get kind information added since they're both kind monomorphic.

comment:76 Changed 3 years ago by oerjan

Priority: normalhighest

Sorry, but GHC 7.10.1 is still vulnerable.

-- This exploit still works in GHC 7.10.1.
-- By Shachaf Ben-Kiki, Ørjan Johansen and Nathan van Doorn

{-# LANGUAGE Safe #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}

import Data.Typeable

type E = (:~:)
type PX = Proxy (((),()) => ())
type PY = Proxy (() -> () -> ())

data family F p a b

newtype instance F a b PX = ID (a -> a)
newtype instance F a b PY = UC (a -> b)

{-# NOINLINE ecast #-}
ecast :: E p q -> f p -> f q
ecast Refl = id

supercast :: F a b PX -> F a b PY
supercast = case cast e of
    Just e' -> ecast e'
  where
    e = Refl
    e :: E PX PX

uc :: a -> b
uc = case supercast (ID id) of UC f -> f

comment:77 Changed 3 years ago by diatchki

Hm, I think I can see what might be the issue, in fact there might be 2:

  • () :: * and () :: Constraint will end up having the same representation
  • Have to look at how we compute type reps for odd rank-2 types like ((),()) => ()

I'll have a go at a fix.

comment:78 in reply to:  77 Changed 3 years ago by oerjan

Replying to diatchki:

Hm, I think I can see what might be the issue, in fact there might be 2:

  • () :: * and () :: Constraint will end up having the same representation
  • Have to look at how we compute type reps for odd rank-2 types like ((),()) => ()

I'll have a go at a fix.

Although the automatic currying makes it disappear in this particular example, tuples like ((),()) also get the same representation as * and Constraint. I guess you currently need the () case to build any others, but I'm not sure if that should be counted on. (I also guess this all means Richard was right.)

comment:79 in reply to:  45 Changed 3 years ago by oerjan

Replying to goldfire:

I believe a sufficiently smart solver should be able to do this without difficulty.

After all the discussion way above, I'll just point out now that the current implementation isn't one of those. I guess it was too much to hope for in such a hurried situation. For example, it breaks on the following expression (with PolyKinds, thanks to Shachaf):

typeOf :: Typeable a => Proxy a -> TypeRep

It seems here that it cannot deduce Typeable (Proxy a) from Typeable a when the kind isn't known at compile time.

More seriously, I think the current TypeRep for Typeable (a :: k) doesn't contain enough information to extract the KindRep for k, much less to decompose it, even if the solver were to try. It seems to have been designed such that type application of known Typeable types (with known kinds) will work almost effortlessly, but anything fancier is impossible.

Ironically I thought (with my convoluted attempts to represent everything in 7.8 types) that type application would be the main thing forcing kind decomposition to be implemented for handling currently existing code, but this representation simply bypasses that. And I guess if no one else has complained then that is currently enough for people's needs.

comment:80 Changed 3 years ago by thoughtpolice

Milestone: 7.12.17.10.2

comment:81 Changed 3 years ago by simonpj

Milestone: 7.10.27.12.1

Iavor, how's it going?

Simon

comment:82 Changed 3 years ago by simonpj

Milestone: 7.12.17.10.2

comment:83 Changed 3 years ago by RyanGlScott

Cc: ryan.gl.scott@… added

comment:84 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 7b042d5adabdb0fc06286db1a7f9cbf1e9fd1fbf/ghc:

Do not allow Typeable on constraints (Trac #9858)

The astonishingly-ingenious trio of
Shachaf Ben-Kiki, Ørjan Johansen and Nathan van Doorn
managed to persuade GHC 7.10.1 to cough up unsafeCoerce.

That is very bad. This patch fixes it by no allowing Typable
on Constraint-kinded things.  And that seems right, since
it is, in effect, a form of impredicative polymorphism,
which Typeable definitely doesn't support.

We may want to creep back in the direction of allowing
Typeable on constraints one day, but this is a good
fix for now, and closes a terrible hole.

comment:85 Changed 3 years ago by simonpj

Status: newmerge
Test Case: typecheck/should_fail/T9858a, should_run/T9858b

OK I think I have fixed this. Again.

Shachaf, Orjan, Nathan: you are very very clever.

Merge to 7.10 branch

Simon

comment:86 Changed 3 years ago by goldfire

Simon, I see how your fix eliminates the problem, but do you know what caused it in the first place?

It might be a tad drastic to just forbid Typeable instances over constraints. For example, should Dict (Show Foo) be Typeable? I think it's reasonable to assume so.

comment:87 Changed 3 years ago by ekmett

Giving up Typeable for Constraint seems very sad. =(

comment:88 Changed 3 years ago by oerjan

Looking at that fix, I'm not sure exactly what types trigger isConstraintKind k (does it include unapplied Show, say?), but wouldn't baking that single Bool test result into the TypeRep also fix things without making Constraints unTypeable?

Also, I am guessing you still technically have "Typeable (=>)" with identical TypeRep as ->, although since they're different kinds I don't see how to exploit that - but that's what we thought of the () thing first. :P

comment:89 Changed 3 years ago by ekmett

Rather than just say it is sad, let's see if we can tackle this issue head on.

A while back, Simon, you posed a sketch of an idea of how to remove the superkinding / existing type hacks by adding another very simple level we can quantify over.

It could be adapted to address this situation.

Consider a type checker where we've removed *, Constraint and # and made a single unified kind Sort a b where a and b are allowed to range over a binary alphabet, lets consider {T,F} as that alphabet. [*]

Then

* = Sort T T
Constraint = Sort T F
# = Sort F T

and we can talk about the kinds of existing types:

() :: forall a. Sort T a

lets () work as both a Constraint or *.

(,) :: forall a. Sort T a -> Sort T a -> Sort T a

lets us tuple up anything as long as both are *'s or both are Constraints.

Unboxed tuples fit:

(#,#) :: forall a b. Sort a T -> Sort a T -> Sort F T

lets unboxed tuples carry *'s and #'s.

and the existing function overloads fit:

(->) :: forall a b. Sort a T -> Sort b T -> Sort T T

All of this then works without the typechecker ever internally lying to itself which then solves this issue in a principled way, as the Typeable instance can know the full choice of kind without subversion.

This removes all of the hacks where (->) :: * -> * -> * but a -> b might have a and b have kinds other than *, etc. in the typechecker, and lets us talk about (->) Int#, or (,) (Eq Int) which are both types we currently can't write:

ghci> :k (->) Int#

<interactive>:1:6:
    Expecting a lifted type, but ‘Int#’ is unlifted
    In a type in a GHCi command: (->) Int#

I already have to work around the lack of the latter by constructing my own product for constraints.

class (p,q) => p & q
instance (p,q) => p & q

Now I can talk about (&) (Eq Int) :: Constraint -> Constraint, but there is no corresponding partial application trick for (->).

We've already implemented a related trick in Ermine without appreciable impact, our kinds there are a little different, so the details vary a bit.

[*] To prevent weird quantifier abuse, you may want to require each of the arguments of Sort to have different ranges, otherwise Sort a a becomes weird.

comment:90 Changed 3 years ago by oerjan

Shachaf and I experimented a bit, and the fix does *not* prohibit Typeable for unapplied type constructors. Together with the polykinded instance for type application, this can be used to construct, albeit awkwardly, Typeable instances for actual constraints. Example:

shachaf> λ> let foo :: forall a b. (Typeable a, Typeable b) => Proxy a
         -> Proxy b -> Proxy (a b) -> TypeRep; foo _ _ _ = typeRep
         (Proxy :: Proxy (a b)) in foo (Proxy :: Proxy Ord) (Proxy ::
         Proxy Int) (Proxy :: Proxy (Ord Int))
shachaf> Ord Int

It is also possible to tease out constraint tuple constructors with type equalities (OK I'm not sure this was actually tested with HEAD, but I suspect it will work there):

shachaf> > let x :: forall (a :: Constraint -> Constraint -> Constraint)
         b c. (a b c ~ (Ord Int, Show Int)) => TypeRep; x = typeRep
         (Proxy :: Proxy a) in x
lambdabot>  (,)

So my theory is that the only thing this fix *strictly* prohibits is Typeable for types involving nullary constraint constructors, including (). Luckily we don't see a way to get an exploit without (), for now.

comment:91 Changed 3 years ago by oerjan

Although Edward's suggestion is elegant, I am thinking that separating Typeable (() :: Constraint) and Typeable (() :: *), in the same way as promoted constructors have been separated from identically named datatypes, is all that is needed to stop this bug without outlawing Typeable constraints.

I think it is impossible to construct two types of the same kind with identical TypeReps without using the kind ambiguity of ().

Although intuitively, Typeable for tuple constructors and -> vs. => should also be separated, just in case. But the former only pass *on* kind ambiguity, while the latter *merge* it. Only () can create it in such a way that it can be merged back (by ->/=>) later.

Which means ->/=> is also necessary, I guess, so if you wanted to outlaw the most impredicative Typeables, you could outlaw just "Typeable ((=>) ...)" instead.

comment:92 Changed 3 years ago by oerjan

Let me elaborate on my previous comment, especially the first suggestion, since my hunch is that it requires the smallest changes to implement to get back constraint Typeables:

  • Instead of prohibiting constraint Typeables, detect the specific case of Typeable (() :: Constraint) and give it a different instance from Typeable (() :: *).

Why is this not less secure than the current fix?

As shown in comment 90, the current fix only effectively prohibits Typeable constraints for nullary constraint constructors.

For other constraints, while ordinary users are greatly inconvenienced, an attacker can instead get the instances for all the constructors used (only the exact kind of Constraint is disallowed, not e.g. * -> Constraint) and put them together with type application, whose Typeable instance needs to be polymorphic and therefore cannot reasonably check for Constraint kinds.

All nullary constructors other than () are either kind monomorphic or have kind parameters to distinguish the TypeReps, so they are useless to an attacker.

How is it better?

It allows Typeable for constraints, which some people think are useful.

My feeling is that constraints, especially used as type parameters, shouldn't be considered impredicative except possibly if they contain =>.

Prohibiting this case was the 3rd suggestion, but my hunch is that this is a more complicated change, and might, if desired, be better done with an overall overhaul disallowing => more uniformly in the same contexts as quantified types, including disallowing splitting a => b into a type application.

How does it still seem a bit awkward?

It still allows some types to have identical TypeReps, like (,) :: * -> * -> * and (,) :: Constraint -> Constraint -> Constraint. This is no change from the current fix, though.

Fixing this entirely was the 2nd suggestion. It might perhaps be implemented directly, although my hunch is that it requires more work, because it needs checking for partial applications and thus more complicated kinds. I assume Edward's suggestion automatically implies this.

How is it sufficient?

With either my suggestion or the currently implemented fix, although some types still have identical TypeReps, I believe they can never have identical kinds as well, and all cast operations require the actual kinds of the compared Typeables to be equal.

Proposition: If two types t and u have the property:

  • t and u are distinct as Haskell types, but have the same TypeRep under the pre-fix system, and either both have the same kind or one has kind * and the other has kind Constraint;

then one of the following holds:

  • They have two corresponding type arguments with the same property.
  • They are, in some order, () :: * and () :: Constraint.

Proof: If at least one of t and u does not have as its tycon one of the kind-ambiguous types (), (,), ..., (->), (=>), then to have equal TypeReps, their tycons and lists of kindreps must be identical, and the types themselves and all their arguments must have corresponding kinds. Thus to be different as types two of their corresponding arguments must have the property.

If the tycons are kind-ambiguous then any arguments must have kind either * or Constraint. With no arguments, with the exception of (), the types must have different kinds that are not * or Constraint, a contradiction. Otherwise, the kinds of the tycons are determined by the kinds of the first arguments, and for t and u to be distinct, there must be two corresponding arguments with the property.


To justify the possibility of the 3rd alternative suggestion as well, the above proof can be adjusted to show that if the kinds of t and u are equal, then types of the form a -> c and b => c must appear as corresponding arguments at some step. This is because all the other options preserve whether the kinds of the arguments are equal or different.

comment:93 Changed 3 years ago by goldfire

After some discussion, we propose the following:

  • Restore Typeable for constraints.
  • Forbid Typeable for types with =>, as those types are higher-rank-ish.
  • Ensure that the TypeReps for () :: * and () :: Constraint are distinct, and similarly for higher arities.

This seems to solve the problems stated here.

For what it's worth, I agree the statements in comment:92, but we can do the trick for all arities, not just 0.

comment:94 Changed 3 years ago by diatchki

This should be fixed in HEAD now. Please give it a whirl, and let me know if you run into any more problems. The implementation should be what Richard discribed:

  • Constraints are OK
  • Impredicative types are not OK (not even things like Eq Int => Int)
  • Constraint and normal tuples should have different representations at all arities.

A side-note: I couldn't figure out how to write the type constructor (,) :: Constraint -> Constraint -> Constraint, so I had to get creative with the testing. Is that intentional?

comment:95 Changed 3 years ago by simonpj

In conversation we had the staggeringly lovely idea of writing a bunch of classes thus:

class (c1,c2) => (,) c1 c2
class (c1,c2,c3) => (,,) c1 c2 c3

etc. I have written the class constructors prefix to stress that we are defining a class (,) etc, but we could equally well say

class (c1,c2) => (c1,c2)   -- Ha ha ha

Now the point is this:

  • c1 and c2 are simply superclasses of the class (c1,c2).
  • The defined class (,), of course, has kind Constraint -> Constraint -> Constraint.
  • This class is distinct from the data type (,). It is just spelled the same way (confusingly perhaps, but that ship has sailed).
  • All the usual rules for superclasses apply. If you have the class (c1,c2) then you can extract the superclasses (c1,c2).
  • If you grep for TuplePred in GHC you'll find quite a bit of code. All of this can be deleted; the existing superclass machinery will do the job just fine.

I like this.

comment:96 Changed 3 years ago by simonpj

Comment for comment:94. Merge to stable branch

commit d8d541d85defcf3bbbddaeee8cfac70b74f47ffc
Author: Iavor S. Diatchki <diatchki@galois.com>
Date:   Thu Apr 16 11:13:24 2015 -0700

    Fixes (hopefully!) T9858
    
    The changes are:
      1. No impredicative types in `Typeable`
      2. Distinguish normal tuples, from tuples of constraints.


>---------------------------------------------------------------

d8d541d85defcf3bbbddaeee8cfac70b74f47ffc
 compiler/deSugar/DsBinds.hs                        |  6 +++-
 compiler/typecheck/TcInteract.hs                   | 34 +++++++++-------------
 testsuite/tests/typecheck/should_fail/T9858b.hs    | 10 +++++++
 .../tests/typecheck/should_fail/T9858b.stderr      |  8 +++++
 testsuite/tests/typecheck/should_fail/all.T        |  1 +
 testsuite/tests/typecheck/should_run/T9858c.hs     | 19 ++++++++++++
 testsuite/tests/typecheck/should_run/T9858c.stdout |  1 +
 testsuite/tests/typecheck/should_run/all.T         |  1 +
 8 files changed, 58 insertions(+), 22 deletions(-)

comment:97 Changed 3 years ago by oerjan

Looking at the fix, I suspect it still does not disallow constructing Typeable (Eq Int => Int) by roundabout means - the test seems to be only for the fully applied form, not the lone => constructor. However, with all the tuple constructors properly disambiguated, I don't think there's an exploit any more.

I just realized my proof above doesn't handle kinds of -> variants like * -> # -> *. But I'm not aware of any way to create an ambiguous TypeRep of possible kind #, so it should hopefully be fine.

comment:98 Changed 3 years ago by diatchki

Well, => is not really a type-constructor, but rather a syntactic form. So I don't think it should ever appear alone, or partially applied, in a Haskell program.

If we ever promoted it to an actual type-constructor status---which is an interesting idea---I think that we should assign it its own type-constructor and stop reusing the function-space constructor.

comment:99 in reply to:  98 ; Changed 3 years ago by oerjan

Replying to diatchki:

Well, => is not really a type-constructor, but rather a syntactic form. So I don't think it should ever appear alone, or partially applied, in a Haskell program.

It doesn't have to appear literally alone. You can already extract a partially applied form, although seemingly not the "constructor" itself.

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}

import Data.Typeable

f :: Proxy (a b) -> Proxy a
f _ = Proxy

g = f (Proxy :: Proxy (Eq Int => Int))

h :: Proxy a -> Proxy (a Bool)
h _ = Proxy

i = h g
*Main> :t g
g :: Proxy (* -> *) ((->) (Eq Int))
*Main> :t i
i :: Proxy * (Eq Int => Bool)

Once you have a partially applied form, you can get Typeable instances for the parts, and then compose them, as shown in comment 90.

Interestingly, GHC internally ensures (and I don't know whether this is a bug or an intended feature) that if you try to extract the (=>) *itself*, you get (->) :: * -> * -> * instead, and a kind matching error. The same applies to -> if you try to pattern match away an unlifted argument type. But in both cases, you can pattern match away a final *lifted* argument type to get a partially applied (->) with an argument of strange kind.

comment:100 Changed 3 years ago by simonpj

Under the fix of comment:96, the line

g = f (Proxy :: Proxy (Eq Int => Int))

would be rejected because there is no Typeable (Eq Int => Int). So I think it looks fine as-is, don't you?

Simon

comment:101 in reply to:  100 ; Changed 3 years ago by oerjan

Replying to simonpj:

Under the fix of comment:96, the line

g = f (Proxy :: Proxy (Eq Int => Int))

would be rejected because there is no Typeable (Eq Int => Int). So I think it looks fine as-is, don't you?

That example wasn't using Typeable, it was just to demonstrate decomposing and rebuilding, which then can be used to circumvent the lack of literal Typeable (Eq Int => Int) (Thanks to int-e for help in testing this with HEAD):

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}

module ConTyp where

import Data.Typeable

f :: Proxy (a b) -> Proxy a
f _ = Proxy

g = f (Proxy :: Proxy (Eq Int => Int))

h :: Proxy a -> Proxy (a Bool)
h _ = Proxy

i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
i p = typeRep p

j = i (h g)

Which in GHCi gives:

> j
Eq Int -> Bool

comment:102 in reply to:  101 Changed 3 years ago by oerjan

We just realized you don't need much more than i there:

> i (Proxy :: Proxy (Eq Int => Int))
Eq Int -> Int

comment:103 Changed 3 years ago by simonpj

Sigh. ImpredicativeTypes certainly causes a lot of pain given that it's a feature that doesn't work and is unsupported.

The problem here is that we should never unify (c => t) with a b, as happens in the call i (Proxy :: Proxy (Eq Int => Int)). Here what happens when I fix this:

T9858.hs:24:8: error:
    Couldn't match type `Eq Int => Int' with `a0 b0'
    Expected type: Proxy (a0 b0)
      Actual type: Proxy (Eq Int => Int)
    In the first argument of `i', namely
      `(Proxy :: Proxy (Eq Int => Int))'
    In the expression: i (Proxy :: Proxy (Eq Int => Int))
    In an equation for `j': j = i (Proxy :: Proxy (Eq Int => Int))

And that seems entirely reasonable.

Thank you - you are amazingly good at exposing my inadequate thinking. Keep it up! (Meanwhile I'll plug this hole tomorrow.)

comment:104 Changed 3 years ago by ekmett

Removing the ability to unify (c => t) works for me. I have no uses of that in the constraints package, and it doesn't make a whole lot of sense anyways, as it really is a syntactic form.

On the other hand, I have plenty of uses now of Typeable for Constraint kinded things.

comment:105 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In c0b5adbd1a04dd1c7916c1240e50a936e826136d/ghc:

Do not decompose => (Trac #9858)

We really don't want to unify (a b) with (Eq a => ty).
The ever-ingenious Oerjan discovered this problem;
see comment:101 in Trac #9858.

See Note [Decomposing fat arrow c=>t] in Type.hs

comment:106 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 932f08677ca07f1793398e4c3456b81359728483/ghc:

Test Trac #9858 comment:101

comment:107 Changed 3 years ago by simonpj

Test Case: typecheck/should_fail/T9858a, should_run/T9858btypecheck/should_fail/T9858a,b,c; should_run/T9858b

comment:108 Changed 3 years ago by simonpj

Are we finally done with this ticket? Can we close it? oerjan?!

comment:109 Changed 3 years ago by oerjan

Well I could continue to quibble about the current design's intrinsic lack of support for my strange test cases in the discussion of comments 43 - 47 and the IMO more reasonable one in comment 79. Of course I was trying to imagine maximal backwards compatibility there.

However, I realize the current design is much less complicated, and apparently works for what people actually do.

I don't see any further actual exploits at this time. :)

comment:110 Changed 3 years ago by simonpj

I think these examples will start to work when we get polykinded typeable, which is a consequence of what Richard is doing on his branch.

What would be useful is if you produce a fresh set of test cases that you think should work, but don't. You can probably extract them from the 100 comments above, but I'd like to know what your short-list is! In fact make them into a new ticket, then we won't lose track. This one is too long and digressive now.

comment:111 in reply to:  99 Changed 3 years ago by oerjan

I made a new ticket #10343 for this.

comment:112 Changed 3 years ago by dterei

Cc: dterei added

comment:113 Changed 3 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Alright, all four of these commits are now merged to ghc-7.10 - thanks everyone!

comment:114 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 130e93aab220bdf14d08028771f83df210da340b/ghc:

Refactor tuple constraints

Make tuple constraints be handled by a perfectly ordinary
type class, with the component constraints being the
superclasses:
    class (c1, c2) => (c2, c2)

This change was provoked by

  #10359  inability to re-use a given tuple
          constraint as a whole

  #9858   confusion between term tuples
          and constraint tuples

but it's generally a very nice simplification. We get rid of
 -  In Type, the TuplePred constructor of PredTree,
    and all the code that dealt with TuplePreds
 -  In TcEvidence, the constructors EvTupleMk, EvTupleSel

See Note [How tuples work] in TysWiredIn.

Of course, nothing is ever entirely simple. This one
proved quite fiddly.

- I did quite a bit of renaming, which makes this patch
  touch a lot of modules. In partiuclar tupleCon -> tupleDataCon.

- I made constraint tuples known-key rather than wired-in.
  This is different to boxed/unboxed tuples, but it proved
  awkward to have all the superclass selectors wired-in.
  Easier just to use the standard mechanims.

- While I was fiddling with known-key names, I split the TH Name
  definitions out of DsMeta into a new module THNames.  That meant
  that the known-key names can all be gathered in PrelInfo, without
  causing module loops.

- I found that the parser was parsing an import item like
      T( .. )
  as a *data constructor* T, and then using setRdrNameSpace to
  fix it.  Stupid!  So I changed the parser to parse a *type
  constructor* T, which means less use of setRdrNameSpace.

  I also improved setRdrNameSpace to behave better on Exact Names.
  Largely on priciple; I don't think it matters a lot.

- When compiling a data type declaration for a wired-in thing like
  tuples (,), or lists, we don't really need to look at the
  declaration.  We have the wired-in thing!  And not doing so avoids
  having to line up the uniques for data constructor workers etc.
  See Note [Declarations for wired-in things]

- I found that FunDeps.oclose wasn't taking superclasses into
  account; easily fixed.

- Some error message refactoring for invalid constraints in TcValidity

comment:115 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In ffc21506894c7887d3620423aaf86bc6113a1071/ghc:

Refactor tuple constraints

Make tuple constraints be handled by a perfectly ordinary
type class, with the component constraints being the
superclasses:
    class (c1, c2) => (c2, c2)

This change was provoked by

  #10359  inability to re-use a given tuple
          constraint as a whole

  #9858   confusion between term tuples
          and constraint tuples

but it's generally a very nice simplification. We get rid of
 -  In Type, the TuplePred constructor of PredTree,
    and all the code that dealt with TuplePreds
 -  In TcEvidence, the constructors EvTupleMk, EvTupleSel

See Note [How tuples work] in TysWiredIn.

Of course, nothing is ever entirely simple. This one
proved quite fiddly.

- I did quite a bit of renaming, which makes this patch
  touch a lot of modules. In partiuclar tupleCon -> tupleDataCon.

- I made constraint tuples known-key rather than wired-in.
  This is different to boxed/unboxed tuples, but it proved
  awkward to have all the superclass selectors wired-in.
  Easier just to use the standard mechanims.

- While I was fiddling with known-key names, I split the TH Name
  definitions out of DsMeta into a new module THNames.  That meant
  that the known-key names can all be gathered in PrelInfo, without
  causing module loops.

- I found that the parser was parsing an import item like
      T( .. )
  as a *data constructor* T, and then using setRdrNameSpace to
  fix it.  Stupid!  So I changed the parser to parse a *type
  constructor* T, which means less use of setRdrNameSpace.

  I also improved setRdrNameSpace to behave better on Exact Names.
  Largely on priciple; I don't think it matters a lot.

- When compiling a data type declaration for a wired-in thing like
  tuples (,), or lists, we don't really need to look at the
  declaration.  We have the wired-in thing!  And not doing so avoids
  having to line up the uniques for data constructor workers etc.
  See Note [Declarations for wired-in things]

- I found that FunDeps.oclose wasn't taking superclasses into
  account; easily fixed.

- Some error message refactoring for invalid constraints in TcValidity

- Haddock needs to absorb the change too; so there is a submodule update

comment:116 Changed 2 years ago by Ben Gamari <ben@…>

In bef2f03e/ghc:

Generate Typeable info at definition sites

This patch implements the idea floated in Trac #9858, namely that we
should generate type-representation information at the data type
declaration site, rather than when solving a Typeable constraint.

However, this turned out quite a bit harder than I expected. I still
think it's the right thing to do, and it's done now, but it was quite
a struggle.

See particularly

 * Note [Grand plan for Typeable] in TcTypeable (which is a new module)
 * Note [The overall promotion story] in DataCon (clarifies existing stuff)

The most painful bit was that to generate Typeable instances (ie
TyConRepName bindings) for every TyCon is tricky for types in ghc-prim
etc:

 * We need to have enough data types around to *define* a TyCon
 * Many of these types are wired-in

Also, to minimise the code generated for each data type, I wanted to
generate pure data, not CAFs with unpackCString# stuff floating about.

Performance
~~~~~~~~~~~
Three perf/compiler tests start to allocate quite a bit more. This isn't
surprising, because they all allocate zillions of data types, with
practically no other code, esp. T1969

 * T3294:   GHC allocates 110% more (filed #11030 to track this)
 * T1969:   GHC allocates 30% more
 * T4801:   GHC allocates 14% more
 * T5321FD: GHC allocates 13% more
 * T783:    GHC allocates 12% more
 * T9675:   GHC allocates 12% more
 * T5642:   GHC allocates 10% more
 * T9961:   GHC allocates 6% more

 * T9203:   Program allocates 54% less

I'm treating this as acceptable. The payoff comes in Typeable-heavy
code.

Remaining to do
~~~~~~~~~~~~~~~

 * I think that "TyCon" and "Module" are over-generic names to use for
   the runtime type representations used in GHC.Typeable. Better might be
   "TrTyCon" and "TrModule". But I have not yet done this

 * Add more info the the "TyCon" e.g. source location where it was
   defined

 * Use the new "Module" type to help with Trac Trac #10068

 * It would be possible to generate TyConRepName (ie Typeable
   instances) selectively rather than all the time. We'd need to persist
   the information in interface files. Lacking a motivating reason I have
   not done this, but it would not be difficult.

Refactoring
~~~~~~~~~~~
As is so often the case, I ended up refactoring more than I intended.
In particular

 * In TyCon, a type *family* (whether type or data) is repesented by a
   FamilyTyCon
     * a algebraic data type (including data/newtype instances) is
       represented by AlgTyCon This wasn't true before; a data family
       was represented as an AlgTyCon. There are some corresponding
       changes in IfaceSyn.

     * Also get rid of the (unhelpfully named) tyConParent.

 * In TyCon define 'Promoted', isomorphic to Maybe, used when things are
   optionally promoted; and use it elsewhere in GHC.

 * Cleanup handling of knownKeyNames

 * Each TyCon, including promoted TyCons, contains its TyConRepName, if
   it has one. This is, in effect, the name of its Typeable instance.

Requires update of the haddock submodule.

Differential Revision: https://phabricator.haskell.org/D757

comment:117 Changed 2 years ago by Ben Gamari <ben@…>

In 91c6b1f5/ghc:

Generate Typeable info at definition sites

This is the second attempt at merging D757.

This patch implements the idea floated in Trac #9858, namely that we
should generate type-representation information at the data type
declaration site, rather than when solving a Typeable constraint.

However, this turned out quite a bit harder than I expected. I still
think it's the right thing to do, and it's done now, but it was quite
a struggle.

See particularly

 * Note [Grand plan for Typeable] in TcTypeable (which is a new module)
 * Note [The overall promotion story] in DataCon (clarifies existing
stuff)

The most painful bit was that to generate Typeable instances (ie
TyConRepName bindings) for every TyCon is tricky for types in ghc-prim
etc:

 * We need to have enough data types around to *define* a TyCon
 * Many of these types are wired-in

Also, to minimise the code generated for each data type, I wanted to
generate pure data, not CAFs with unpackCString# stuff floating about.

Performance
~~~~~~~~~~~
Three perf/compiler tests start to allocate quite a bit more. This isn't
surprising, because they all allocate zillions of data types, with
practically no other code, esp. T1969

 * T1969:    GHC allocates 19% more
 * T4801:    GHC allocates 13% more
 * T5321FD:  GHC allocates 13% more
 * T9675:    GHC allocates 11% more
 * T783:     GHC allocates 11% more
 * T5642:    GHC allocates 10% more

I'm treating this as acceptable. The payoff comes in Typeable-heavy
code.

Remaining to do
~~~~~~~~~~~~~~~

 * I think that "TyCon" and "Module" are over-generic names to use for
   the runtime type representations used in GHC.Typeable. Better might
be
   "TrTyCon" and "TrModule". But I have not yet done this

 * Add more info the the "TyCon" e.g. source location where it was
   defined

 * Use the new "Module" type to help with Trac Trac #10068

 * It would be possible to generate TyConRepName (ie Typeable
   instances) selectively rather than all the time. We'd need to persist
   the information in interface files. Lacking a motivating reason I
have
   not done this, but it would not be difficult.

Refactoring
~~~~~~~~~~~
As is so often the case, I ended up refactoring more than I intended.
In particular

 * In TyCon, a type *family* (whether type or data) is repesented by a
   FamilyTyCon
     * a algebraic data type (including data/newtype instances) is
       represented by AlgTyCon This wasn't true before; a data family
       was represented as an AlgTyCon. There are some corresponding
       changes in IfaceSyn.

     * Also get rid of the (unhelpfully named) tyConParent.

 * In TyCon define 'Promoted', isomorphic to Maybe, used when things are
   optionally promoted; and use it elsewhere in GHC.

 * Cleanup handling of knownKeyNames

 * Each TyCon, including promoted TyCons, contains its TyConRepName, if
   it has one. This is, in effect, the name of its Typeable instance.

Updates haddock submodule

Test Plan: Let Harbormaster validate

Reviewers: austin, hvr, goldfire

Subscribers: goldfire, thomie

Differential Revision: https://phabricator.haskell.org/D1404

GHC Trac Issues: #9858

comment:118 Changed 2 years ago by bgamari

Description: modified (diff)
Differential Rev(s): Phab:D652Phab:D652, Phab:D757

comment:119 Changed 22 months ago by bgamari

comment:120 Changed 13 months ago by bgamari

There are some relevant performance comments in #12748.

Note: See TracTickets for help on using tickets.