Specialize function via annotation

I’m trying to work with fetch:

fetch 
  :: forall input output thruIn thruOut headers
  . Union input thruIn (HighlevelRequestOptions headers String) 
  => Union output thruOut UnsafeRequestOptions 
  => ToCoreRequestOptions input output 
  => String 
  -> { | input }
  -> Aff Response

and I’m trying to make a helper function that can expand the functionality (by e.g., making the Aff fail if not response.ok). So I’m trying to make a function that still has the generic input, output, headers etc., and call fetch but the compiler isn’t letting me. To illustrate the problem I can say:

fetch2 
  :: forall input output thruIn thruOut headers
  . Union input thruIn (HighlevelRequestOptions headers String) 
  => Union output thruOut UnsafeRequestOptions 
  => ToCoreRequestOptions input output 
  => String 
  -> { | input } 
  -> Aff Response
fetch2 = fetch

and this won’t compile even though the annotation for fetch2 is identical to fetch, because it’ll say that the first Union constraint is not available and it contains unknown type variables and needs an annotation. I’m pretty sure this is related to the fact that the implementation of fetch still compiles if you completely remove the first constraint - it’s not needed by the implementation at all.

I’ve found out that I can work around the problem by copying the implementation of fetch and adding a parameter of type Proxy thruIn. So I could have:

fetchWithProxy
  :: forall input output thruIn thruOut headers
   . Union input thruIn (HighlevelRequestOptions headers String)
  => Union output thruOut CoreRequest.UnsafeRequestOptions
  => ToCoreRequestOptions input output
  => Proxy thruIn
  -> String
  -> { | input }
  -> Aff Response
fetchWithProxy _ url r = do
  -- this implementation just copied directly from fetch
  request <- liftEffect $ new url $ Request.convert r
  cResponse <- Promise.toAffE $ Response.promiseToPromise <$> Core.fetch request
  pure $ Response.convert cResponse

fetch2 
  :: forall input output thruIn thruOut headers
  . Union input thruIn (HighlevelRequestOptions headers String) 
  => Union output thruOut UnsafeRequestOptions 
  => ToCoreRequestOptions input output 
  => String 
  -> { | input }
  -> Aff Response
fetch2 = fetchWithProxy (Proxy :: _ thruIn)

Anyway I’d really like to be able to do this without copying the implementation of fetch and just somehow tell the compiler that my thruIn needs to be the same as fetch’s thruIn. So maybe something like

fetch2 
  :: forall input output thruIn thruOut headers
  . Union input thruIn (HighlevelRequestOptions headers String) 
  => Union output thruOut UnsafeRequestOptions 
  => ToCoreRequestOptions input output 
  => String 
  -> { | input }
  -> Aff Response
fetch2 = (fetch :: ?_)

But I can’t figure out a syntax that will let me do this. thruIn only shows up in the constraints, and not at all in any of the input/output types.

Any advice where to go with this to avoid having to copy the source of fetch just to get that proxy in there?

Here’s a more minimal reproduction:

type R a = (a :: a)

f :: ∀ input x a.
  Union input x (R a) =>
  Record input -> Unit
f _ = unit

f2 :: ∀ input x a.
  Union input x (R a) =>
  Record input -> Unit
f2 a = f a

Here f2 won’t compile because of a missing constraint.
Interestingly, if I get rid of the type a and use a concrete type, then it’s fine

type R a = (a :: a)

f :: ∀ input x.
  Union input x (R Int) =>
  Record input -> Unit
f _ = unit

f2 :: ∀ input x.
  Union input x (R Int) =>
  Record input -> Unit
f2 a = f a

So I think the solution I’m looking for is how in f2 to annotate f to tell it how to specialize its type variables (so that I can make them match the type variables for f2)

I wonder if Visible Type Applications could help with this? This compiles

import Prelude

import Prim.Row (class Union)
import Type.Prelude (Proxy(..))

type R :: forall k. k -> Row k
type R a = (a :: a)

f
  :: forall input x a
   . Union input x (R a)
  => Proxy x
  -> Record input
  -> Unit
f _ _ = unit

f2
  :: forall input x a
   . Union input x (R a)
  => Record input
  -> Unit
f2 a = f (Proxy :: Proxy x) a

(Try PureScript link) so I wonder if with VTA syntax you might be able to have

f
  :: forall input @x a
   . Union input x (R a)
  => Record input
  -> Unit
f _ = unit

f2
  :: forall input x a
   . Union input x (R a)
  => Record input
  -> Unit
f2 a = f @x a

Edit: oops! I realized on closer read you have the Proxy solution in your first post. I’m not sure of an alternative without using Proxy or VTA (which seems like would also require a change in the underlying fetch library).

Oh wow, it looks like VTA is coming in 0.15.10? I guess I haven’t been keeping track. That’s exciting!

Anyway, yeah I was afraid I wouldn’t have a solution without changing the source of fetch. Thanks