GHC cannot deduce an instance exists despite being mentioned in a quantified constraint

Question

I have the following program:

{-# language MultiParamTypeClasses #-}
{-# language PolyKinds #-}
{-# language QuantifiedConstraints #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language TypeApplications #-}
{-# language UndecidableInstances #-}

module Control.IO.GWeave where

import Generics.Kind


newtype HigherOrder e m a =
  HigherOrder ( e m a )


weaveFromTo
  :: forall m n e a code.
     ( GenericK e ( LoT2 n a )
     , GenericK e ( LoT2 m a )
     , GWeave ( RepK e ) m n ( LoT2 m a ) ( LoT2 n a )
     )
  => ( forall x. m x -> n x ) -> HigherOrder e m a -> HigherOrder e n a
weaveFromTo eta ( HigherOrder a ) =
    HigherOrder ( toK ( gweave @_ @m @n @( LoT2 m a ) @( LoT2 n a ) eta ( fromK a ) ) )

class GWeave f ( m :: * -> * ) ( n :: * -> * ) as bs where
  gweave :: ( forall x. m x -> n x ) -> f as -> f bs

class Effect e where
  weave :: ( forall x. m x -> n x ) -> e m a -> e n a

instance
  ( forall n a. GenericK e ( LoT2 n a )
  , forall m n a. GWeave ( RepK e ) m n ( LoT2 m a ) ( LoT2 n a )
  ) => Effect ( HigherOrder e ) where
  weave eta =
    weaveFromTo eta

In this, I have class Effect e where weave = .... I want to use DerivingVia to provide instances of Effect for any data type that is an instance of GenericK (from the kind-generics library on Hackage). This is perfectly doable, and weaveFromTo is the bulk of the work. The last step is to simply say instance Effect (HigherOrder e) where weave f = weaveFromTo f. However, GHC seems to refuse to accept this, even if I add the necessary constraints onto the instance declaration for Effect (HigherOrder e):

• Could not deduce (GWeave (RepK e) m n (LoT2 m a) (LoT2 n a))
  from the context: (forall (n :: * -> *) (a :: k).
                     GenericK e (LoT2 n a),
                     forall (m :: * -> *) (n :: * -> *) (a :: k).
                     GWeave (RepK e) m n (LoT2 m a) (LoT2 n a))
    bound by an instance declaration:
               forall k (e :: (* -> *) -> k -> *).
               (forall (n :: * -> *) (a :: k). GenericK e (LoT2 n a),
                forall (m :: * -> *) (n :: * -> *) (a :: k).
                GWeave (RepK e) m n (LoT2 m a) (LoT2 n a)) =>
               Effect (HigherOrder e)

I'm unable to work out why GHC is unhappy. Can anyone see the problem? The code above should work provided you have kind-generics installed.

user_1236540 · Answer

You don't need to use a newtype, just moving the type family application RepK e outside of the quantification makes it work (the change is in the line marked as (!)):

instance
  ( forall n a. GenericK e ( LoT2 n a )
  , r ~ ( RepK e )  -- (!)
  , forall m n a. GWeave r m n ( LoT2 m a ) ( LoT2 n a )
  ) => Effect ( HigherOrder e ) where
  weave eta =
    weaveFromTo eta

This is because, by design, instances in Haskell cannot use type families. That is, you cannot write an instance that looks like:

instance Eq (RepK e) where ...

Quantified constraints inherit that restriction, since they introduce sort of "local instances". You can find more information in the GHC tracker and in this Reddit thread.

As an extra piece of advice, everytime you use RepK e in kind-generics, always give it an explicit name outside of any quantification. Otherwise you end up with weird errors like the one you got.

user_74497 · Answer

Ok, I found the solution - I have to package up RepK into a newtype:

weaveFromTo
  :: forall m n e a code.
     ( GenericK e ( n :&&: a :&&: LoT0 )
     , GenericK e ( m :&&: a :&&: LoT0 )
     , GWeave ( WrappedRepK e ) m n ( LoT2 m a ) ( LoT2 n a )
     )
  => ( forall x. m x -> n x ) -> HigherOrder e m a -> HigherOrder e n a
weaveFromTo eta ( HigherOrder a ) =
    HigherOrder ( toK ( unWrapRepK ( gweave @_ @m @n @( LoT2 m a ) @( LoT2 n a ) eta ( WrapRepK @e ( fromK a ) ) ) ) )

class GWeave f ( m :: * -> * ) ( n :: * -> * ) as bs where
  gweave :: ( forall x. m x -> n x ) -> f as -> f bs

instance GWeave ( RepK e ) m n ( LoT2 m a ) ( LoT2 n a ) => GWeave ( WrappedRepK e ) m n ( LoT2 m a ) ( LoT2 n a ) where
  gweave eta ( WrapRepK a ) =
    WrapRepK ( gweave eta a )


instance
  ( forall n a. GenericK e ( LoT2 n a )
  , forall m n a. GWeave ( WrappedRepK e ) m n ( m :&&: a :&&: LoT0 ) ( n :&&: a :&&: LoT0 )
  ) => Effect ( HigherOrder e ) where
  weave eta =
    weaveFromTo eta

newtype WrappedRepK r a =
  WrapRepK { unWrapRepK :: RepK r a }

I think it's because RepK is a type family, so... something goes screwy? I'd love to know more about why this fix works.

GHC cannot deduce an instance exists despite being mentioned in a quantified constraint

2 Answers