error involving uverb

[fisx]

If you copy the following code into Servant.API.UVerb.Union:

data User tag = User

type XS tag = Union '[User tag, ()]

f :: forall tag m. Applicative m => User tag -> m (XS tag)
f usr = either respond respond $ (undefined :: Either () (User tag))

respond ::
  forall (x :: *) (xs :: [*]) (f :: * -> *).
  (Applicative f, IsMember x xs) =>
  x ->
  f (Union xs)
respond = pure . inject . I

you get:

Servant/API/UVerb/Union.hs:159:24: warning: [-Wdeferred-type-errors]
    • Expected one of:
          '[User tag, ()]
      But got:
          User tag
    • In the second argument of ‘either’, namely ‘respond’
      In the expression: either respond respond
      In the expression:
        either respond respond $ (undefined :: Either () (User tag))
    |
159 | f usr = either respond respond $ (undefined :: Either () (User tag))
    |                        ^^^^^^^

Without the phantom tag, it compiles fine. I would have expected it to compile both ways.

[fisx]

Now I also get this:

Servant/API/UVerb/Union.hs:154:24: warning: [-Wdeferred-type-errors]
    • Overlapping instances for UElem (User tag0) '[User tag, ()]
        arising from a use of ‘respond’
      Matching instances:
        instance [overlapping] forall a (x :: a) (xs :: [a]) (x' :: a).
                               UElem x xs =>
                               UElem x (x' : xs)
          -- Defined at Servant/API/UVerb/Union.hs:109:30
        instance [overlapping] forall a (x :: a) (xs :: [a]).
                               UElem x (x : xs)
          -- Defined at Servant/API/UVerb/Union.hs:104:30
      (The choice depends on the instantiation of ‘k0, tag0, k, tag’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the second argument of ‘either’, namely ‘respond’
      In the expression: either respond respond
      In the expression:
        either respond respond $ (undefined :: Either () (User tag))
    |
154 | f usr = either respond respond $ (undefined :: Either () (User tag))
    |                        ^^^^^^^

Even if i turn on incoherent instances.

[arianvp]

My feeling is that our type-error type-family is hiding the true error in your first example. Could you try commenting out our friendly error messages and see if the error is more helpful?

[mheinzel]

I think the type equality operator (==) chokes on the type variable.

ghci> type family CheckEqual a b :: Constraint where { CheckEqual a b = If (a == b) (() :: Constraint) (a ~ b) }
ghci> test :: CheckEqual a b => a -> b -> IO () ; test _ _ = putStrLn "equal types!"
ghci> test [True] [False]
equal types!
ghci> test [] []

<interactive>:43:1: error:
    • Could not deduce: If (a0 == a1) (() :: Constraint) ([a0] ~ [a1])
        arising from a use of ‘test’
    • In the expression: test [] []
      In an equation for ‘it’: it = test [] []

[arianvp]

That makes sense. [] :: forall a. [a] and [] :: forall b. [b] are different types and aren't equal. You run into extensionality problems here

[mheinzel]

Ah, yeah, not the best example. But it can be adapted to be closer to the original issue (having the same type variable on both sides), still showing the same problem:

Prelude Data.Type.Equality Data.Type.Bool Data.Kind> test :: CheckEqual a a => a  -> IO () ; test _ _ = putStrLn "equal!"
Prelude Data.Type.Equality Data.Type.Bool Data.Kind> test []

<interactive>:45:1: error:
    • Could not deduce: If (a0 == a0) (() :: Constraint) ([a0] ~ [a0])
        arising from a use of ‘test’
    • In the expression: test []
      In an equation for ‘it’: it = test []

So == works differently to ~, it doesn't try to unify variables and it doesn't consider a variable to be equal to itself.

[arianvp]

Yeh checking equality on polymorphic types does not work in Haskell.

Hence you can only call respond on monomorphic types or you need to delay the equality check up. e.g.:

f :: forall tag m. (Elem (User tag) [User tag, ()] , Applicative m) => User tag -> m (Union '[User tag, ()])
f usr = either respond respond $ (undefined :: Either () (User tag))

[arianvp]

Yeh (==) is a type-level function; not some special unification thing:

https://hackage.haskell.org/package/base-4.14.0.0/docs/src/Data.Type.Equality.html#%3D%3D

[mheinzel]

Yes, propagating the constraint up is a decent workaround.

[fisx]

Cool, thanks for solving this! We should add this to the cookbook before closing the issue. I'll assign it to myself!