GitLab

Summary

following code:

{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynonyms, FlexibleContexts, AllowAmbiguousTypes, ScopedTypeVariables #-}

module Lib where

import GHC.Exts
import GHC.TypeLits
import Data.Proxy

data a ::: b = a ::: b

class Pair f where
  type Left  f :: a
  type Right f :: b

instance Pair (a '::: b) where
  type Left  (a '::: b) = a
  type Right (a '::: b) = b

class    NC (x :: k)
instance NC (x :: k)

data L1 c f xs where
  LC :: c x => f x -> L1 c f xs -> L1 c f (x ': xs)
  LN :: L1 c f '[]

class (c1 (Left f), c2 (Right f)) => PairC c1 c2 f
instance (c1 x, c2 y) => PairC c1 c2 (x '::: y)

data f1 :*: f2 :: (kx ::: ky) -> * where
  (:*:) :: f1 x -> f2 y -> (f1 :*: f2) (x '::: y)

pairC :: forall c1 c2 x y e . (c1 x, c2 y) => (PairC c1 c2 (x '::: y) => e) -> e
pairC e = e

type Foo t = L1 (PairC KnownSymbol NC) (Proxy :*: t)
pattern Foo :: forall s a t xs . KnownSymbol s => KnownSymbol s => Proxy s -> t a -> Foo t xs -> Foo t (s '::: a ': xs)
pattern Foo p t xs <- LC (p :*: t) xs where
  Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)

Results in this compile error:

/home/ryba/ghc-bug/src/Lib.hs:38:46: error:
    • Could not deduce (PairC KnownSymbol NC (s '::: a))
        arising from a use of ‘LC’
      from the context: KnownSymbol s
        bound by the signature for pattern synonym ‘Foo’
        at src/Lib.hs:(37,1)-(38,61)
      or from: PairC KnownSymbol NC (s '::: a)
        bound by a type expected by the context:
                   PairC KnownSymbol NC (s '::: a) =>
                   L1 (PairC KnownSymbol NC) (Proxy :*: t) ((s '::: a) : xs)
        at src/Lib.hs:38:45-61
    • In the fifth argument of ‘pairC’, namely ‘(LC (p :*: t) xs)’
      In the expression: pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
      In an equation for ‘Foo’:
          Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
   |
38 |   Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
   |                                              ^^^^^^^^^^^^^^^

Which basically boils down to "could not deduce a from a"

Environment

• GHC version used: 8.10.2
• stack resolver=nightly-2020-09-14

Optional:

• Operating System: Ubuntu
• System Architecture: x86-64