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 RyanGlScott

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.

comment:2 Changed 18 months ago by josef

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 RyanGlScott

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 goldfire

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 RyanGlScott

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 Changed 18 months ago by goldfire

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 in reply to:  6 Changed 18 months ago by RyanGlScott

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 simonpj

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 Iceland_jack

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
Last edited 18 months ago by Iceland_jack (previous) (diff)

comment:10 Changed 18 months ago by Iceland_jack

Keywords: wipT2893 added

Relevant discussion at ticket:14734#comment:5

comment:11 Changed 18 months ago by simonpj

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 RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.