Opened 10 months ago

Closed 6 months ago

Last modified 6 months ago

#14845 closed feature request (fixed)

TypeInType, index GADT by constraint witness

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: dependent/should_fail/T14845_fail1,T14845_fail2
Blocked By: Blocking:
Related Tickets: #13895, #15215, #15282 Differential Rev(s): Phab:D4728
Wiki Page:

Description

Just wondering if it would ever make sense to allow or use constraints like this

{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}

import Data.Kind

data Struct :: (k -> Constraint) -> (k -> Type) where
  S :: cls a => Struct cls a

data Foo a where
  F :: Foo (S::Struct Eq a)
$ ghci -ignore-dot-ghci /tmp/test.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/test.hs, interpreted )

/tmp/test.hs:9:13: error:
    • Illegal constraint in a type: cls0 a0
    • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
      In the type ‘Foo (S :: Struct Eq a)’
      In the definition of data constructor ‘F’
  |
9 |   F :: Foo (S::Struct Eq a)
  |             ^
Failed, no modules loaded.
Prelude> 

Please close the ticket if it doesn't

Change History (22)

comment:1 Changed 10 months ago by Iceland_jack

Summary: TypeInType, index by GADT witnessing constraintTypeInType, index GADT by constraint witness

comment:2 Changed 10 months ago by RyanGlScott

I too have hit this limitation—or rather, I have hit this error message—in #13895. But in the case of #13895, the root of the issue is impredicativity, whereas here I'm not sure that's the case.

I'd be curious to hear goldfire's reasoning for why this restriction is in place, since the source code doesn't have much in the way of an explanation.

comment:3 Changed 10 months ago by simonpj

I think it's this. S is a data constructor with an evidence argument. At the term level we pass evidence to S. But if we promote S we don't have a type-level version of evidence.

So I was going to say "we don't promote S". But then I remembered that TypeInType is supposed to allow GADTs at the type level. So now I'm confused.

comment:4 Changed 10 months ago by goldfire

Technically, we do promote S, but the promoted S can't ever be applied, because we can't produce evidence. Perhaps a better error message is warranted, but until we have real dependent types (and can promote dictionaries), I think we're stuck on this one.

comment:5 Changed 10 months ago by simonpj

Technically, we do promote S, but the promoted S can't ever be applied

Would it not be better (for now anyway) not to promote S?

comment:6 Changed 10 months ago by goldfire

I suppose the difference in promoting and not promoting is in the error message, no?

comment:7 in reply to:  6 Changed 10 months ago by RyanGlScott

Replying to goldfire:

I suppose the difference in promoting and not promoting is in the error message, no?

Indeed. If a tree is promoted in a forest but no one can see it, is it ever really promoted? :)

comment:8 Changed 10 months ago by simonpj

I suppose the difference in promoting and not promoting is in the error message, no?

Indeed! You'll get "Data constructor S can't be used in a type because it's a GADT" or something like tat, rather than the current mysterious one.

comment:9 Changed 10 months ago by goldfire

OK. Then we can just reword the error message. :)

Note that problem isn't that it's a GADT constructor. The problem is that it's a constrained constructor and constraints don't promote.

Ryan, you find it far easier than I to actually get patches sent off -- would you mind tweaking this message? Thanks!

comment:10 Changed 10 months ago by RyanGlScott

But there's a significant wrinkle here. You're proposing that we change the error message to something like Data constructor has a constraint 'cls0 a0', and thus cannot be promoted, yes? But the place where this error message is thrown is tcInstBinders, which is not in any way data-constructor–specific. Indeed, as I mentioned in comment:2, this error message also occurs in the program in #13895, but that doesn't promote any data constructors whatsoever.

So if we change this error message carte blanche, all of a sudden GHC is going to be complaining about data constructors which don't exist.

Last edited 10 months ago by RyanGlScott (previous) (diff)

comment:11 Changed 10 months ago by simonpj

I don't agree with comment:2. This ticket doesn't seem to have anything to do with impredicativity. It just has to do with a constructor that's promoted, but shouldn't be. Doesn't it?

comment:12 Changed 10 months ago by RyanGlScott

This is the test case from #13895:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Foo where

import Data.Data (Data, Typeable)
import Data.Kind

dataCast1 :: forall (a :: Type).
             Data a
          => forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).
             Typeable t
          => (forall d. Data d => c (t d))
          -> Maybe (c a)
dataCast1 _ = undefined
$ /opt/ghc/8.4.1/bin/ghci Bug.hs
GHCi, version 8.4.0.20180224: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo              ( Bug.hs, interpreted )

Bug.hs:11:23: error:
    • Illegal constraint in a type: Typeable k0
    • In the first argument of ‘Typeable’, namely ‘t’
      In the type signature:
        dataCast1 :: forall (a :: Type).
                     Data a =>
                     forall (c :: Type -> Type)
                            (t :: forall (k :: Type). Typeable k => k -> Type).
                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
   |
11 |              Typeable t
   |                       ^

Bug.hs:12:38: error:
    • Illegal constraint in a type: Typeable k0
    • In the first argument of ‘c’, namely ‘(t d)’
      In the type signature:
        dataCast1 :: forall (a :: Type).
                     Data a =>
                     forall (c :: Type -> Type)
                            (t :: forall (k :: Type). Typeable k => k -> Type).
                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
   |
12 |           => (forall d. Data d => c (t d))
   |                                      ^^^

Note that there are no promoted constructors in this program! But changing the error message as per the suggestion in comment:9 means that the new error message for this program would (incorrectly) be:

Data constructor has a constraint `Typeable k0`, and thus cannot be promoted

Since the place where this error message arises, tcInstBinder, has no knowledge of where the constraint comes from (in particular, whether it comes from a promoted constructor or not).

I just want to make sure that if we do change this error message, that we don't degrade the quality of the error message in this program. But I have no idea how tcInstBinder works, so knowing how to propagate the relevant information down into tcInstBinder to make it aware of the provenance of the error message is far above my pay grade.

comment:13 Changed 10 months ago by goldfire

Hmph. You're right. You could always just add a NB: Constrained data constructors cannot be promoted or Have you tried promoting a constrained data constructor?. I don't think people will often trip over this.

The other place to check is in the AGlobal (AConLike (RealDataCon dc)) case in TcHsType.tcTyVar. I don't suppose it would be hard to check if the datacon had constraints. The only access seems to be in the fourth component of a dataConFullSig, but the comments there refer to a dataConDictTheta (now extinct) that could be revived to return this nugget. That might be a better route.

comment:14 Changed 10 months ago by simonpj

OK so there are two things

  • A data constructor should not be promoted if it has a constrained type. This should not be hard to arrange.
  • As comment:12 shows, a kind signature should hove no constraints in it. Surely checkValidType is the place for that check.

By the time we get to tcInstBinder the crime is well past!

comment:15 Changed 10 months ago by goldfire

But equality constraints are OK. Even user-written ones. What about ones hidden behind type synonyms? I think they should be, too.

comment:16 Changed 10 months ago by goldfire

Actually, come to think of it, the check I suggested around dataConFullSig will snag user-written equality constraints, which it shouldn't. For example

data G a where
  MkG :: a ~ Int => G a

should be just fine to promote. So something more delicate will be needed.

comment:17 Changed 7 months ago by RyanGlScott

Differential Rev(s): Phab:D4728
Status: newpatch

Phab:D4728 attempts to provide a better error message when promoting a data constructor with an unpromotable context.

Note that I didn't attempt to change checkValidType in this patch, since that would require a significant amount of plumbing to check whether checkValidType was being called on a type or a kind. I felt that the existing error message from tcInstBinder (which I tweaked slightly in this Diff to say "kind" instead of "type") was sufficient.

This patch also doesn't check for type synonyms, as suggested in comment:15, since that would require changing the checks in tcInstBinder accordingly, and I don't know how to do that. But in any case, this is a solid improvement over the status quo.

comment:18 Changed 6 months ago by simonpj

#15215 (after fixing the bug in that ticket) is another example of the horrible error message reported in the Description.

comment:19 Changed 6 months ago by Simon Peyton Jones <simonpj@…>

In 2f6069c/ghc:

Make better "fake tycons" in error recovery

Consider (Trac #15215)
  data T a = MkT ...
  data S a = ...T...MkT....

If there is an error in the definition of 'T' we add a
"fake type constructor" to the type environment, so that we
can continue to typecheck 'S'.  But we /were not/ adding
a fake anything for 'MkT' and so there was an internal
error when we met 'MkT' in the body of 'S'.

The fix is to add fake tycons for all the 'implicits' of 'T'.
This is done by mk_fake_tc in TcTyClsDecls.checkValidTyCl,
which now returns a /list/ of TyCons rather than just one.

On the way I did some refactoring:

* Rename TcTyDecls.tcAddImplicits to tcAddTyConsToGblEnv
  and make it /include/ the TyCons themeselves as well
  as their implicits

* Some incidental refactoring about tcRecSelBinds. The main
  thing is that I've avoided creating a HsValBinds that we
  immediately decompose.  That meant moving some deck chairs
  around.

NB: The new error message for the regression test T15215
has the opaque error "Illegal constraint in a type:", flagged
in Trac #14845.  But that's the fault of the latter ticket.
The fix here not to blame.

comment:20 Changed 6 months ago by Ben Gamari <ben@…>

In c637541/ghc:

Provide a better error message for unpromotable data constructor contexts

Trac #14845 brought to light a corner case where a data
constructor could not be promoted (even with `-XTypeInType`) due to
an unpromotable constraint in its context. However, the error message
was less than helpful, so this patch adds an additional check to
`tcTyVar` catch unpromotable data constructors like these //before//
they're promoted, and to give a sensible error message in such cases.

Test Plan: make test TEST="T13895 T14845"

Reviewers: simonpj, goldfire, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #13895, #14845

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

comment:21 Changed 6 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: patchclosed
Test Case: dependent/should_fail/T14845_fail1, dependent/should_fail/T14845_fail2

Commit c63754118cf6c3d0947d0c611f1db39c78acf1b7 improves the error message substantially.

As mentioned in comment:4, we can't actually allow this program until dependent types are available.

The remaining task from this ticket is to document how a program like the one in comment:16 desugars into coercions at the Core level. I've opened #15282 for this.

Last edited 6 months ago by RyanGlScott (previous) (diff)

comment:22 Changed 6 months ago by simonpj

Test Case: dependent/should_fail/T14845_fail1, dependent/should_fail/T14845_fail2dependent/should_fail/T14845_fail1,T14845_fail2
Note: See TracTickets for help on using tickets.