VariantF: Ambiguous type variable that seems unambiguous

[woehr]

I'm trying to write a pattern for an EADT type that contains a less general, parameterised EADT type, but I receive the following ambiguous type variable error. I've reproduced the error in a minimum working example, below. In the example, the definition of bar causes the error.

Adding a type annotation (seen on baz) fixes the error. However, it seems obvious to me that the second argument to C' should be a T1 Bool. Thus I'm wondering if it's somehow possible to get the compiler to figure this out itself.

VarBug.hs:23:7: error:
    • Couldn't match type ‘Haskus.Utils.Types.List.Filter
                             (C'F a0 (EADT '[CF Bool, C'F Bool]))
                             (Haskus.Utils.Types.List.RemoveAt1
                                (Haskus.Utils.Types.List.MaybeIndexOf'
                                   1
                                   (C'F a0 (EADT '[CF Bool, C'F Bool]))
                                   '[C'F Bool (Fix (VariantF '[CF Bool, C'F Bool]))])
                                '[CF Bool (Fix (VariantF '[CF Bool, C'F Bool])),
                                  C'F Bool (Fix (VariantF '[CF Bool, C'F Bool]))])’
                     with ‘CF Bool (Fix (VariantF '[CF Bool, C'F Bool]))
                             : Haskus.Utils.Types.List.Filter
                                 (C'F a0 (EADT '[CF Bool, C'F Bool]))
                                 '[C'F Bool (Fix (VariantF '[CF Bool, C'F Bool]))]’
        arising from a use of ‘C'’
      The type variable ‘a0’ is ambiguous
    • In the expression: C' (C True) (C True)
      In an equation for ‘bar’: bar = C' (C True) (C True)
   |
23 | bar = C' (C True) (C True)
   |       ^^^^^^^^^^^^^^^^^^^^

VarBug.hs:23:20: error:
    • Couldn't match type ‘Haskus.Utils.Types.List.Filter
                             (CF Bool (EADT '[CF a0]))
                             (Haskus.Utils.Types.List.RemoveAt1
                                (Haskus.Utils.Types.List.MaybeIndexOf'
                                   0 (CF Bool (EADT '[CF a0])) '[CF a0 (Fix (VariantF '[CF a0])
)])
                                '[CF a0 (Fix (VariantF '[CF a0]))])’
                     with ‘Haskus.Utils.Types.List.Filter
                             (CF Bool (EADT '[CF a0])) '[CF a0 (Fix (VariantF '[CF a0]))]’
        arising from a use of ‘C’
      NB: ‘Haskus.Utils.Types.List.Filter’ is a type function, and may not be injective
      The type variable ‘a0’ is ambiguous
    • In the second argument of ‘C'’, namely ‘(C True)’
      In the expression: C' (C True) (C True)
      In an equation for ‘bar’: bar = C' (C True) (C True)
   |
23 | bar = C' (C True) (C True)
   |                    ^^^^^^
Failed, no modules loaded.

This code produces the error above, but the annotation on baz makes it work:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeOperators #-}

import Haskus.Utils.VariantF
import Prelude

data CF a f = CF a deriving (Functor)
type T1 a = EADT '[CF a]

data C'F a f = C'F f (T1 a) deriving (Functor)
type T2 a = EADT '[CF a, C'F a]

pattern C :: (CF a :<: xs) => a -> EADT xs
pattern C x = VF (CF x)

pattern C' :: (C'F a :<: xs) => EADT xs -> T1 a -> EADT xs
pattern C' x y = VF (C'F x y)

bar :: T2 Bool
bar = C' (C True) (C True)

--baz :: T2 Bool
--baz = C' (C True) (C True :: T1 Bool)

[hsyl20]

That's one of the limitations with the current implementation of Variant: when we have T a :<: '[X, T Int] we don't infer a ~ Int and similarly the other way around. It might be possible to help the type-checker with a compiler plugin but we would still have to deal with some ambiguous cases (e.g., T a :<: '[X, T Int, T Char, b] should infer a ~ (Int, Char or something else depending on b)).

As a workaround you can also use type applications:

bar :: T2 Bool
bar = C' @Bool (C True) (C True)

[woehr]

I see. Thanks for the explanation!

[woehr]

When using types like those of the example with pattern matching, type errors occur due to ambiguous type variables. For example, the following function does not work without -XScopedTypeVariables and the annotations in the pattern. I'm assuming this is the same issue, however type applications cannot be used in this situation. Is there a more convenient way of writing such a function? Also, this ghc ticket seems relevant https://ghc.haskell.org/trac/ghc/ticket/11350.

func :: EADT '[CF Char, C'F Char] -> Int
func (C (_ :: Char)      ) = 1
func (C' _ (_ :: T1 Char)) = 2

[hsyl20]

Also, this ghc ticket seems relevant https://ghc.haskell.org/trac/ghc/ticket/11350.

Yes I'm waiting for this feature to come into GHC to remove type annotations in the pattern. If someone wants to write a GHC proposal for it, it would be great.