Confusing error with QuantifiedConstraints

[deepfire]

First, I apologise in advance, if this is not a valid place for such issues, so please feel free to close this, if that's the case.

The problem is that using QuantifiedConstraints to enforce Code constraint results in a confusing type error, that doesn't appears to make sense.

The goal is to:

1. enforce a particular structure ('[xs])
2. on a type derived from a typeclass parameter (using Code)
3. without introducing a new typeclass parameter (abstracting over detail)

This seems to require QuantifiedConstraints, because:
I. I could find no other way to encode the Code a ~ '[xs] constraint (f.e. Code a ~ '[Head (Code a)] makes GHC blow reduction stack.
II. Code a ~ '[xs] requires a type variable, which I'm hesitant to admit into the typeclass, because of requirement 3

..however, using QuantifiedConstraints to introduce a fresh variable fails in a confusing way:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# OPTIONS_GHC -Wextra -Wno-unused-imports -Wno-unticked-promoted-constructors -Wno-type-defaults -Wno-missing-signatures #-}

module Main where

import           Control.Monad.IO.Class
import qualified GHC.Generics as GHC
import           Generics.SOP
import qualified Generics.SOP as SOP


class    ( GHC.Generic a, SOP.Generic a, HasDatatypeInfo a
         , forall xs. Code a ~ '[xs]) => Foo m a where

instance ( GHC.Generic a, SOP.Generic a, HasDatatypeInfo a
         , forall xs. Code a ~ '[xs]
         , Monad m)                  => Foo m a where

..leads to:

error:
    • Could not deduce: Code a ~ '[xs]
        arising from the superclasses of an instance declaration
      from the context: (GHC.Generic a, HasDatatypeInfo a,
                         forall (xs :: [*]). Code a ~ '[xs], Monad m)
        bound by the instance declaration
        at /run/user/1000/danteazsW1Q.hs:(22,10)-(24,47)
    • In the instance declaration for ‘Foo m a’

..which appears contradictory, because:

1. Code a ~ '[xs] is explicitly stated in the instance
2. There is no indication of type variables not unifying -- i.e. no mismatch between xs and xs0 or somesuch is reported (which is typical when unification fails due to existentials not aligning).

[RyanGlScott]

This is actually a GHC issue in deep disguise. The issue is that on GHC 8.6, QuantifiedConstraints can't be headed by the (~) type constructor—see Trac #15359. (The error message doesn't make this at all obvious, but that's what is going on there.)

That particular restriction has been lifted in GHC HEAD. That being said, your code still won't compile on GHC HEAD for another reason:

../Bug.hs:19:1: error:
    • Illegal type synonym family application ‘Code a’ in instance:
        Code a ~ '[xs]
    • In the quantified constraint ‘forall (xs :: [*]). Code a ~ '[xs]’
      In the context: (GHC.Generic a, Generic a, HasDatatypeInfo a,
                       forall (xs :: [*]). Code a ~ '[xs])
      While checking the super-classes of class ‘Foo’
      In the class declaration for ‘Foo’
   |
19 | class    ( GHC.Generic a, SOP.Generic a, HasDatatypeInfo a
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

../Bug.hs:22:10: error:
    • Illegal type synonym family application ‘Code a’ in instance:
        Code a ~ '[xs]
    • In the quantified constraint ‘forall (xs :: [*]). Code a ~ '[xs]’
      In the instance declaration for ‘Foo m a’
   |
22 | instance ( GHC.Generic a, SOP.Generic a, HasDatatypeInfo a
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

That limitation is due to a much deeper limitation of QuantifiedConstraints, which is summarized here.

[deepfire-pusher]

On the first glance, QuantifiedConstraints seemed like a way to arbitrarily introduce fresh variables on the left side of the typeclass head.

I knew this looked too good to be true!

Thank you for the explanation, Ryan!

[RyanGlScott]

I take it this issue can be closed, then?

[deepfire]

Sure!

[deepfire]

I'll try to use the Simon's Hack at https://ghc.haskell.org/trac/ghc/ticket/14860#comment:1 as a workaround..

[deepfire]

..or even the option by IcelandJack: https://gist.github.com/Icelandjack/aeda8e98214cc52c96230af7b8724d25

[kosmikus]

I don't think I've had a problem with Code a ~ '[Head (Code a)] in the past. Do you have a minimal failing example for this?

And regardless of the error message or GHC bugs, I don't think the quantified constraint could possibly be correct. You'd need an exists, not a forall.

[kosmikus]

I'll reopen this for now because IsProductType is in principle supposed to solve this use case, but it does introduce an additional type variable. In cases where this was undesirable, I've up until now applied the "hack" using Head. But perhaps there should be an out-of-the-box solution that doesn't introduce an additional type variable.

So let's have this discussion at least. We can always close again if there's no clear improvement over the status quo that we could apply.

[deepfire]

I have the Code a ~ '[Head (Code a)] reduction stack blowup error buried inside a fairly tangled piece of code.

I'll try to find some time to extract it, hopefully soon enough..