#13895 closed bug (duplicate)
"Illegal constraint in a type" error - is it fixable?
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler (Type checker) | Version: | 8.0.1 |
Keywords: | TypeInType, ImpredicativeTypes | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | dependent/should_fail/T13895 |
Blocked By: | Blocking: | ||
Related Tickets: | #12045, #14845, #14859 | Differential Rev(s): | Phab:D4728 |
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 (10)
comment:1 Changed 2 years ago by
comment:2 Changed 2 years ago by
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:4 Changed 2 years ago by
Related Tickets: | → #12045 |
---|
comment:5 Changed 19 months ago by
Related Tickets: | #12045 → #12045, #14845 |
---|
comment:6 Changed 16 months ago by
Keywords: | ImpredicativeTypes added |
---|---|
Related Tickets: | #12045, #14845 → #12045, #14845, #14859 |
comment:7 Changed 16 months ago by
Differential Rev(s): | → Phab:D4728 |
---|---|
Status: | new → patch |
Phab:D4728 adds a test case for the latter part of the ticket (catching an illegal use of a constraint in a kind, as in forall (t :: forall (k :: Type). Typeable k => ...)
).
comment:9 Changed 15 months ago by
Resolution: | → duplicate |
---|---|
Status: | patch → closed |
comment:10 Changed 15 months ago by
Milestone: | → 8.6.1 |
---|---|
Test Case: | → dependent/should_fail/T13895 |
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...