Can't disambiguate Tagged. - Polysemy

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

locallycompact

Hi. I'm able to do this:

taggedLookupKV :: forall t k v r a
             . Members '[Tagged t (KVStore k v)] r
            => k
            -> Sem r v
taggedLookupKV k = tag @t @(KVStore k v) (lookupKV @k @v k)

But if I try to add a second store (to say model the one updating the other), then this instantly fails to type check.

taggedLookupKV :: forall t t' k v r a
             . Members '[Tagged t (KVStore k v), Tagged t' (KVStore k v)] r
            => k
            -> Sem r v
taggedLookupKV k = tag @t @(KVStore k v) (lookupKV @k @v k)
    • Could not deduce: Polysemy.Internal.Union.LocateEffect
                          (Tagged t0 (KVStore k4 v)) r
                        ~ '()
      from the context: Members
                          '[Tagged t (KVStore k4 v), Tagged t' (KVStore k4 v)] r
        bound by the type signature for:
                   taggedLookupKV' :: forall k k2 k3 (t :: k) (t' :: k2) k4 v
                                             (r :: [(* -> *) -> * -> *]) (a :: k3).
                                      Members
                                        '[Tagged t (KVStore k4 v), Tagged t' (KVStore k4 v)] r =>
                                      k4 -> Sem r v
      The type variable ‘t0’ is ambiguous
    • In the ambiguity check for ‘taggedLookupKV’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        taggedLookupKV :: forall t t' k v r a.
                           Members '[Tagged t (KVStore k v), Tagged t' (KVStore k v)] r =>
                           k -> Sem r v
Georgi Lyubenov // googleson78

that's how hs type inference for type variables works

Georgi Lyubenov // googleson78

your taggedLookupKV doesn't have an argument which uses t or t'

Georgi Lyubenov // googleson78

so callers will be forced to manually specify what t and t' are, using TypeApplications

Georgi Lyubenov // googleson78

that's why ghc is asking you to enable AllowAmbiguousTypes

Georgi Lyubenov // googleson78

because hs was originally designed with the thought of the user never having to do manual type annotations, and this breaks that "rule"

Georgi Lyubenov // googleson78

if you want to avoid TypeApplications, you can add a Proxy t argument, but usually people prefer TypeApplications because it's less noisy (imo)

locallycompact

Oh ok, so just to clarify if this is the whole prog

prog :: forall t t' k v r. Members '[Input k, Tagged t (KVStore k v), Tagged t' (KVStore k v)] r => Sem r ()
prog = do
  a <- input @k
  z <- tag @t @(KVStore k v) (existsKV @k @v a)
  if z
    then return ()
  else
    do
      x <- tag @t' @(KVStore k v) (lookupKV @k @v a)
      case x of
        Nothing -> return ()
        Just x' -> tag @t @(KVStore k v) (writeKV @k @v a x')

So I turn on ambiguous types then I just have to specify that whenever I use this, which is to be expected anyway.

Georgi Lyubenov // googleson78

oh and of note - I'm pretty sure the first one doesn't complain about ambiguous types only because of the plugin