Here's a simple recursive function:
ignore :: [a] -> ()
ignore [] = ()
ignore (a:as) = ignore as
It is polymorphic, and it is recursive. But, like almost all recursions, whatever type the caller chooses for a, the recursion happens using the same choice for a. That is, we could write this, with ScopedTypeVariables and probably a handful of other extensions:
ignore :: forall a. [a] -> ()
ignore (a:as) = ignore @a as
The term "polymorphic recursion" refers to a very special kind of recursion, where the recursive call chooses a different type for some parameter. The standard example is this one:
data BalancedTree a = Leaf a | Branch (BalancedTree (a, a))
foldBT :: (a -> a -> a) -> BalancedTree a -> a
foldBT f (Leaf a) = a
foldBT f (Branch bt) = uncurry f $ foldBT (\(x, y) (x', y') -> (f x x', f y y')) bt
(For example, foldBT (+) would add all the elements of the tree.)
The special thing here is that the recursive call to foldBT is not recursing over a BalancedTree a -- but over a BalancedTree (a, a) instead. The type has changed, like this:
foldBT :: forall a. (a -> a -> a) -> BalancedTree a -> a
foldBT f (Branch bt) = uncurry f $ foldBT @(a, a) {- N.B. not a! -} (\(x, y) (x', y') -> (f x x', f y y')) bt
It turns out that type inference in the setting that allows this kind of thing is pretty hard. To deal with that, Haskell has a restriction: inferred types always use monomorphic recursion, that is, all recursive calls choose all the same values for the type variables involved. You can still get polymorphic recursion by giving an appropriate type signature, because then inference is not needed.
Now, in your working situation, you write
cmdList :: forall command arg result.
(Param command, Param arg, CmdParams result) =>
command -> [arg] -> result
cmdList command = go . reverse where
-- for clarity, I have chosen fresh type variable names
go :: forall arg' result'. (Param arg', CmdParams result') => [arg'] -> result'
go [] = cmd command
go (arg:args) = go args arg
Notice that in the recursive case, go is being given an extra argument on the right hand side of the equation compared to the left! This is polymorphic recursion; the result type is slowly accumulating extra arguments.
go (arg:args) = go @arg' @(arg' -> result') {- N.B. not result'! -} args arg
This means that in the base case,
go [] = cmd command
the type of cmd may be different depending on how many arguments there are in the list! In other words, you can think of events happening in this order: first the user chooses a command type, an argument type, and a result type; then you traverse the list and choose a different result type that accepts more arguments; then you call cmd with that newly chosen result type.
Compare the version that doesn't work:
go :: (Param arg, CmdParams result) => result -> [arg] -> result
go b [] = b
go b (arg:args) = go b args arg
In this version, a choice has been lost; first the user chooses a result type, then you traverse the list and choose the same result type as the user did; then you use their b of that type. But this is a problem -- they may not have chosen the right number of arguments for that list, and even if they did, it's not really reasonable to expect the compiler to be able to know that statically!
This explains the occurs check error you've gotten: for go to work right in this setting, its b argument has to be able to accept an arbitrary number of arguments, and there just isn't any single type that does that.
It also explains why you cannot use foldr: foldr is implemented with monomorphic recursion. It is probably possible to create a variant of foldr using RankNTypes that could sit in this spot, but I suspect it's more work than it's worth.
And, by the way, I think you can make your refactoring work, though I'm not 100% because I haven't installed shell-monad to check this. But it would look something like this:
go :: (Param arg, CmdParams result) => (forall result'. CmdParams result') -> [arg] -> result
-- same implementation as before
The key here is that putting the extra forall there forces the first b argument to be polymorphic; this lets you choose result' to be a suitably-many-arguments variant of result when you get to the base case.
