How to use a proxy in Haskell? (probably using a higher-rank types extension)
ghc, haskell, proxy
Solution
You just need to explicitly specify that the function `f0` must be polymorphic by adding the universal quantifier `forall ga.` to your type signatures:
call_f0 :: Gen gb => (forall ga. Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, PROXY gb Char)]
test :: Gen gb => (forall ga. Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, gb Char)]
Otherwise, GHC will put an implicit `forall ga.` at the outermost level, meaning that the caller would get to decide which `ga` should be used, while GHC has correctly deduced that these functions must be able to choose themselves that `ga` should be `PROXY gb`.
In other words, when using `RankNTypes` to require a polymorphic argument, you must always use an explicit quantifier to specify this.
Problem
For the last few months, I've been putting some serious effort into learning Haskell - previously, I was a seemingly perpetual newbie with a very limited knowledge of the basics. While trying to put my new knowledge into practice on few-steps-up-from-hello-world projects, I keep finding that I want to use proxy-like patterns based on type classes. The first couple of times, when I figured out why it wasn't working, I dismissed it as "OK - I may not find a single idiomatic Haskell replacement, but odds are the problem here is that I'm using the wrong approach for the language". But what I've found is that I really really don't like not being able to do proxy-like things. Trying to get a deeper understanding of why I couldn't use a proxy, after lots of experimenting, I finally figured out that with GHCs higher rank types extension, perhaps I can have proxies. But I still can't quite make it work, and I'm not sure why. Here is the code for the best I've managed... ``` {-# LANGUAGE RankNTypes #-} module Test where -- Simple type class based on parser combinators. class Gen g where get :: g x -> [(x, g x)] instance Gen [] where get [] = [] get (x:xs) = [(x, xs)] -- Proxy type - holds a pair containing... -- - a value of some type that supports Gen -- - a function to indicate when an item should be skipped newtype PROXY nestedgen x = Proxy (nestedgen x, x -> Bool) proxyskip :: Gen nestedgen => PROXY nestedgen r -> Bool proxyskip (Proxy (g, predf)) = case get g of [] -> False ((r,_):_) -> predf r proxyget :: Gen nestedgen => PROXY nestedgen r -> [(r, PROXY nestedgen r)] proxyget pr@(Proxy (sg, predf)) = if proxyskip pr then [(r2, g2) | (_, g1) <- get sg, (r2,g2) <- proxyget (Proxy (g1, predf))] else [(r3, Proxy (g3, predf)) | (r3,g3) <- get sg] -- Instance of Gen for PROXY - get skips items where appropriate instance Gen nestedgen => Gen (PROXY nestedgen) where get = proxyget -- Test "parser" -- Get the specified number of items, providing them as a list (within -- the list of nondeterministic (result, state) pairs). getN :: Gen g => Int -> g x -> [([x], g x)] getN n g | (n < 0) = error "negative n" | (n == 0) = [([], g)] | True = [(r1:r2, g2) | (r1, g1) <- get g, (r2, g2) <- getN (n-1) g1] -- Wrap some arbitrary "parser" in a PROXY that skips over the letter 'l' proxyNotL :: Gen gb => gb Char -> PROXY gb Char proxyNotL gg = (Proxy (gg, \ch -> (ch /= 'l'))) call_f0 :: Gen gb => (Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, PROXY gb Char)] call_f0 f0 g0 = f0 (proxyNotL g0) test :: Gen gb => (Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, gb Char)] test f0 g0 = [(r, g2) | (r, Proxy (g2, _)) <- call_f0 f0 g0] ``` The last remaining error occurs on the line `call_f0 f0 g0 = f0 (proxyNotL g0)`... ``` [1 of 1] Compiling Test ( Test.hs, Test.o ) Test.hs:44:21: Could not deduce (ga ~ PROXY gb) from the context (Gen gb) bound by the type signature for call_f0 :: Gen gb => (Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, PROXY gb Char)] at Test.hs:44:1-33 `ga' is a rigid type variable bound by the type signature for call_f0 :: Gen gb => (Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, PROXY gb Char)] at Test.hs:44:1 Expected type: ga Char Actual type: PROXY gb Char In the return type of a call of `proxyNotL' In the first argument of `f0', namely `(proxyNotL g0)' In the expression: f0 (proxyNotL g0) ``` Looking at the problematic function... ``` call_f0 :: Gen gb => (Gen ga => ga Char -> [(r, ga Char)]) -> gb Char -> [(r, PROXY gb Char)] call_f0 f0 g0 = f0 (proxyNotL g0) ``` The `f0` function is (if I understand higher rank types correctly) a polymorphic function passed as a parameter, with type `Gen ga => ga Char -> [(r, ga Char)]`. In translating-to-C terms, the caller has passed in a function pointer, but has not supplied the vtable pointer. The `proxyNotL` function returns something of type `PROXY gb Char`, and there's an instance declaration `instance Gen nestedgen => Gen (PROXY nestedgen) where ...`, so that `PROXY gb Char` instances `Gen` provided `gb` instances `Gen`, which it does according to the type signature for `call_f0`. Basically, as far as I can tell, GHC should say "can I provide the vtable that `f0` requires... hmmm... yes, since `PROXY gb` instances `Gen`, and I know about `PROXY` and `gb`, yes I can". So... why is GHC refusing to unify `ga` and `Proxy gb`? Why is GHC refusing to call a polymorphic function, with an argument value that should be supported by the polymorphic type of that function? Or alternatively, what am I completely misunderstanding here?