Opened 18 months ago
Last modified 16 months ago
#14968 new bug
QuantifiedConstraints: Can't be RHS of type family instances
Reported by: | josef | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #9269 | Differential Rev(s): | |
Wiki Page: |
Description
Here's a type family that I tried to write using QuantifiedConstraints.
{-# LANGUAGE TypeOperators #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE QuantifiedConstraints #-} module QCTypeInstance where import GHC.Exts (Constraint) type family Functors (fs :: [(* -> *) -> * -> *]) :: Constraint type instance Functors '[] = (() :: Constraint) type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)
Unfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition.
$ ../ghc-wip/T2893/inplace/bin/ghc-stage2 --interactive QCTypeInstance.hs GHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted ) QCTypeInstance.hs:13:15: error: • Illegal polymorphic type: forall (f :: * -> *). Functor f => Functor (t f) • In the type instance declaration for ‘Functors’ | 13 | type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts) | ^^^^^^^^
Would it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do?
Change History (12)
comment:1 Changed 18 months ago by
Related Tickets: | → #9269 |
---|
comment:2 Changed 18 months ago by
Right. I'm aware to the difficulties discussed in ticket #9269. My questions is really whether we can hope to do better when the result kind of a type family is of kind Constraint
rather than *
.
comment:3 Changed 18 months ago by
I'm not sure what the return kind has anything to do with this. Ultimately, the issue is impredicativity, which is going to be a problem regardless of whether you're working over *
, Constraint
(as in your example), Bool
(as in the example in https://ghc.haskell.org/trac/ghc/ticket/9269#comment:1), or something else.
comment:4 Changed 18 months ago by
Actually, I think the OP's use case should be OK. There is a big difference between the type (forall x. x -> x, Int)
and the constraint (forall x. A x => B x, Show x)
. The former is an impredicative use of the (,)
constructor, while the second is not considered to be so. I think this is a simple case of updating the validity checker to allow the new thing. :)
comment:5 Changed 18 months ago by
I'm lost. Is there some aspect of quantified constraints that would make this OK:
type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)
But not this (from https://ghc.haskell.org/trac/ghc/ticket/9269#comment:1)?
type instance Foo True = forall a. a -> a -> a
comment:6 follow-up: 7 Changed 18 months ago by
The challenge impredicativity causes is in knowing where there is an invisible parameter. (I'm pretty sure that's the challenge, at least.) So if x :: ty
and we don't know whether or not ty
is a forall
-type, we have a problem. This simply doesn't happen with constraints, so we avoid the challenge.
comment:7 Changed 18 months ago by
Replying to goldfire:
This simply doesn't happen with constraints, so we avoid the challenge.
Really? Is there some sort of invariant in GHC that upholds this claim? You can certainly have x :: ty
where ty :: Constraint
in Core, so this claim is quite surprising to me.
comment:8 Changed 18 months ago by
The challenge is knowing whether a type (F t)
might reduce to a polytype. Currently that cannot happen. Allowing it to happen gives all the same problems as impredicativity in general. So I think that allowing a forall on the RHS of a type instance
is a big step.
comment:9 Changed 18 months ago by
This compiles
type family Functors (fs :: [(Type -> Type) -> Type -> Type]) :: Constraint where Functors '[] = () Functors (t:ts) = (LvlUp Functor t, Functors ts) class (forall x. cls x => cls (f x)) => LvlUp cls f instance (forall x. cls x => cls (f x)) => LvlUp cls f
comment:10 Changed 18 months ago by
Keywords: | wipT2893 added |
---|
Relevant discussion at ticket:14734#comment:5
comment:11 Changed 18 months ago by
Well comment:9 doesn't have foralls on the RHS of a type family, so should be fine. I'm not sure how/why it's relevant to this thread though!
comment:12 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
This is a particular occurrence of a more general restriction, which is explained in https://ghc.haskell.org/trac/ghc/ticket/9269#comment:1. So yes, there are fundamental difficulties here that have yet to be worked out.