Opened 3 weeks ago

Last modified 2 weeks 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 2 weeks ago by

### comment:2 Changed 2 weeks 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 weeks ago by

Related Tickets: | → #12045 |
---|

**Note:**See TracTickets for help on using tickets.

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...