So, I'm trying to implement a polyvariadic ZipWithN as described here. Unfortunately, Paczesiowa's code seems to have been compiled with outdated versions of both ghc and HList, so in the process of trying to understand how it works, I've also been porting it up to the most recent versions of both of those (ghc-7.8.3 and HList-0.3.4.1 at this time). It's been fun.
Anyways, I've run into a bug that google isn't helping me fix for once, in the definition of an intermediary function curryN'. In concept, curryN' is simple: it takes a type-level natural number N (or, strictly speaking, a value of that type), and a function f whose first argument is an HList of length N, and returns an N-ary function that takes makes an HList out of its first N arguments, and returns f applied to that HList. It's curry, but polyvariadic.
It uses three helper functions/classes:
The first is ResultType/resultType, as I've defined here. resultType takes a single function as an argument, and returns the type of that function after applying it to as many arguments as it will take. (Strictly speaking, again, it returns an undefined value of that type).
For example:
ghci> :t resultType (++)
resultType (++) :: [a]
ghci> :t resultType negate
resultType negate :: (ResultType a result, Num a) => result
(The latter case because if a happens to be a function of type x -> y, resultType would have to return y. So it's not perfect applied to polymorphic functions.)
The second two are Eat/eat and MComp/mcomp, defined together (along with curryN') in a single file (along with the broken curryN') like this.
eat's first argument is a value whose type is a natural number N, and returns a function that takes N arguments and returns them combined into an HList:
ghci> :t eat (hSucc (hSucc hZero))
eat (hSucc (hSucc hZero)) :: x -> x1 -> HList '[x, x1]
ghci> eat (hSucc (hSucc hZero)) 5 "2"
H[5, "2"]
As far as I can tell it works perfectly. mcomp is a polyvariadic compose function. It takes two functions, f and g, where f takes some number of arguments N. It returns a function that takes N arguments, applies f to all of them, and then applies g to f. (The function order parallels (>>>) more than (.))
ghci> :t (,,) `mcomp` show
(,,) `mcomp` show :: (Show c, Show b, Show a) => a -> b -> c -> [Char]
ghci> ((,,) `mcomp` show) 4 "str" 'c'
"(4,\"str\",'c')"
Like resultType, it "breaks" on functions whose return types are type variables, but since I only plan on using it on eat (whose ultimate return type is just an HList), it should work (Paczesiowa seems to think so, at least). And it does, if the first argument to eat is fixed:
\f -> eat (hSucc (hSucc hZero)) `mcomp` f
works fine.
curryN' however, is defined like this:
curryN' n f = eat n `mcomp` f
Trying to load this into ghci, however, gets this error:
Part3.hs:51:1:
Could not deduce (Eat n '[] f0)
arising from the ambiguity check for ‘curryN'’
from the context (Eat n '[] f,
MComp f cp d result,
ResultType f cp)
bound by the inferred type for ‘curryN'’:
(Eat n '[] f, MComp f cp d result, ResultType f cp) =>
Proxy n -> (cp -> d) -> result
at Part3.hs:51:1-29
The type variable ‘f0’ is ambiguous
When checking that ‘curryN'’
has the inferred type ‘forall f cp d result (n :: HNat).
(Eat n '[] f, MComp f cp d result, ResultType f cp) =>
Proxy n -> (cp -> d) -> result’
Probable cause: the inferred type is ambiguous
Failed, modules loaded: Part1.
So clearly eat and mcomp don't play as nicely together as I would hope. Incidentally, this is significantly different from the kind of error that mcomp (+) (+1) gives, which complains about overlapping instances for MComp.
Anyway, trying to find information on this error didn't lead me to anything useful - with the biggest obstacle for my own debugging being that I have no idea what the type variable f0 even is, as it doesn't appear in any of the type signatures or contexts ghci infers.
My best guess is that mcomp is having trouble recursing through eat's polymorphic return type (even though what that is is fixed by a type-level natural number). But if that is the case, I don't know how I'd go about fixing it.
Additionally (and bizarrely to me), if I try to combine Part1.hs and Part2.hs into a single file, I still get an error...but a different one
Part3alt.hs:59:12:
Overlapping instances for ResultType f0 cp
arising from the ambiguity check for ‘curryN'’
Matching givens (or their superclasses):
(ResultType f cp)
bound by the type signature for
curryN' :: (MComp f cp d result, Eat n '[] f, ResultType f cp) =>
Proxy n -> (cp -> d) -> result
at Part3alt.hs:(59,12)-(60,41)
Matching instances:
instance result ~ x => ResultType x result
-- Defined at Part3alt.hs:19:10
instance ResultType y result => ResultType (x -> y) result
-- Defined at Part3alt.hs:22:10
(The choice depends on the instantiation of ‘cp, f0’)
In the ambiguity check for:
forall (n :: HNat) cp d result f.
(MComp f cp d result, Eat n '[] f, ResultType f cp) =>
Proxy n -> (cp -> d) -> result
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘curryN'’:
curryN' :: (MComp f cp d result, Eat n [] f, ResultType f cp) =>
Proxy n -> (cp -> d) -> result
Failed, modules loaded: none.
Again with the mysterious f0 type variable. I'll admit that I'm a little bit over my head here with all this typehackery, so if anyone could help me figure out what exactly the problem here is, and, more importantly, how I can fix it (if it is, hopefully, possible), I'd be incredibly grateful.
Final note: the reasons that the two files here are called Part1 and Part3 is that Part2 contains some auxiliary functions used in zipWithN, but not curryN'. For the most part they work fine, but there are a couple of oddities that I might ask about later.
