Opened 3 months ago

Last modified 3 months ago

#13895 new bug

"Illegal constraint in a type" error - is it fixable?

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #12045 Differential Rev(s):
Wiki Page:

Description

I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:

dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
             Typeable t
          => (forall d. Data d => c (t d))
          -> Maybe (c a)

But this doesn't typecheck:

    • Could not deduce (Typeable (t k0))
      from the context: (Data a, Typeable (t k))
        bound by the type signature for:
                   dataCast1 :: forall a.
                                Data a =>
                                forall k (c :: * -> *) (t :: forall k1. k1 -> *).
                                Typeable (t k) =>
                                (forall d. Data d => c (t * d)) -> Maybe (c a)
        at NewData.hs:(170,3)-(173,26)
      The type variable ‘k0’ is ambiguous
    • In the ambiguity check for ‘dataCast1’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        dataCast1 :: forall a.
                     Data a =>
                     forall k (c :: * -> *) (t :: forall k1. k1 -> *).
                     Typeable (t k) =>
                     (forall d. Data d => c (t * d)) -> Maybe (c a)
      In the class declaration for ‘Data’
    |
170 |   dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

This makes sense, since GHC has no way to conclude that the k in t's kind is also Typeable. I tried to convince GHC of that fact:

dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).
             Typeable t
          => (forall d. Data d => c (t d))
          -> Maybe (c a)

But this also doesn't work:

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

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

At this point, I'm stuck, since I have no idea how to work around this Illegal constraint in a type error. This error message appears to have originated as a part of the TypeInType patch, since there's even a test case checking for this behavior.

But is this a fundamental limitation of kind equalities? Or would it be possible to lift this restriction?

Change History (4)

comment:1 Changed 3 months ago by goldfire

You want impredicativity. But you can't have it. :)

The problem is more visible when we expand your Typeable t constraint to write explicitly the kind argument: Typeable (forall k. k -> Type) t, which uses a polytype to instantiate a datatype parameter.

I'm afraid I don't have a workaround to suggest...

comment:2 Changed 3 months ago by RyanGlScott

Interesting. Simon once commented that using TypeApplications to call a polymorphic function at a polymorphic type fell under a safe subset of ImpredicativeTypes (that ought not require bringing in the other baggage that ImpredicativeTypes implies). If we had this capability, would Typeable @(forall k. k -> Type) t be a thought GHC could think? (I realize that we don't yet have visible kind applications, but you get the idea.)

comment:3 Changed 3 months ago by goldfire

Yes, that would work nicely.

comment:4 Changed 3 months ago by Iceland_jack

Note: See TracTickets for help on using tickets.