Reify existential instance type parameter

Question

I've got some code like this:

{-# LANGUAGE AllowAmbiguousTypes #-}
module Foo where

import Data.Proxy

class Foo x y
class Bar x y
class Baz x y
  where
  baz :: Proxy x -> Proxy y -> ()

instance (Foo a v, Bar b v) => Baz a b
  where
  baz _ _ = ()

instance Foo String String
instance Bar Int String

Now I actually want to use that Baz instance, so I write:

test :: Proxy String -> Proxy Int -> ()
test = baz

But of course there is an ambiguous "existential" v type parameter that I have not yet fixed to String (and there's no fundeps), so I get:

[typecheck] [E] /tmp/foo/src/Main.hs:20:8: error:
    • Ambiguous type variable ‘v1’ arising from a use of ‘baz’
      prevents the constraint ‘(Foo [Char] v1)’ from being solved.
      Probable fix: use a type annotation to specify what ‘k1’,
                                                          ‘v1’ should be.
      These potential instance exist:
        one instance involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: baz
      In an equation for ‘test’: test = baz

But how can I actually fix that type variable? I can't see a way to fix it using visible type application, because for example the following doesn't work:

test2 :: Proxy String -> Proxy Int -> ()
test2 = baz @String @Int @String -- is there some variation of this that would work?

I also can't see a way to use an explicit type annotation to fix that type parameter. Have I written an instance that is impossible to actually use?

dfeuer dfeuer · Accepted Answer · 2020-07-06T01:25:54

It is indeed impossible to use that instance. When you call baz, you can supply a and b, but not v. v would have to be determined by some combination of superclass and instance constraints, and it is not.

You should be able to patch this up various places. Try either

instance s ~ String => Foo String s

or

instance s ~ String => Bar Int s

for example.

Reify existential instance type parameter

1 Answers