Skip to content

Could not deduce instance with two quantified constraints

Summary

I'm running into an issue where GHC is not able to deduce the required constraint even though I believe there is a way to deduce it.

Steps to reproduce

{-# LANGUAGE QuantifiedConstraints #-}

type f ~> g = forall x. f x -> g x

class (forall f. Functor f => Functor (h f)) => HFunctor h where
  hmap :: (f ~> g) -> (h f ~> h g)

class (forall m. Monad m => Monad (h m), HFunctor h) => HMonad h where
  hreturn :: Monad m => m ~> h m
  hdnib :: (Monad m, Monad n) => (m ~> h n) -> h m ~> h n

bar :: (HMonad h, Monad f) => (Functor (h f) => c) -> c
bar x = x
Test.hs:14:9: error:
    • Could not deduce (Functor (h f)) arising from a use of ‘x’
      from the context: (HMonad h, Monad f)
        bound by the type signature for:
                   bar :: forall (h :: (* -> *) -> * -> *) (f :: * -> *) c.
                          (HMonad h, Monad f) =>
                          (Functor (h f) => c) -> c
        at Test.hs:13:1-55
    • In the expression: x
      In an equation for ‘bar’: bar x = x
   |
14 | bar x = x
   |         ^

Expected behavior

It should be able to deduce:

               HMonad t
              ----------
              HFunctor t                   Monad n
------------------------------------      ---------
forall f. Functor f => Functor (t f)      Functor n
---------------------------------------------------
                  Functor (t n)

Or

           HMonad t
--------------------------------
forall m. Monad m => Monad (t m)      Monad n
---------------------------------------------
                   Monad (t n)
                  -------------
                  Functor (t n)

Environment

  • GHC version used: 9.2.1
Edited by Jaro Reinders
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information