Skip to content

Pattern synonym succeeds with constraint tuple, but fails with curried constraints

My pattern synonym is accepted if I pass the constraints as a tuple, but fails if I pass the constraints one after the other (curried).

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

import Data.Proxy
import GHC.TypeLits

newtype Modulo a (n :: Nat) = Mod a

pattern Works :: forall n a. (Integral a , KnownNat n) => a -> Modulo a n
pattern Works a <- Mod a where
  Works a = Mod $ mod a $ fromIntegral $ natVal $ Proxy @n

-- No instance for (KnownNat n) arising from the "provided" constraints
pattern Fails :: forall n a. Integral a => KnownNat n => a -> Modulo a n
pattern Fails a <- Mod a where
  Fails a = Mod $ mod a $ fromIntegral $ natVal $ Proxy @n

-- No instance for (Integral a) arising from the "provided" constraints
pattern Fails2 :: forall n a. KnownNat n => Integral a => a -> Modulo a n
pattern Fails2 a <- Mod a where
  Fails2 a = Mod $ mod a $ fromIntegral $ natVal $ Proxy @n

So, isn't C1 => C2 => a -> b the same as (C1, C2) => a -> b?

This is on GHC 8.0 - GHC 9.2.2 (same error always).

Maybe related: #12975

Edited by Andreas Abel
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information