Thanks for the suggestion. I have added NoPolyKinds to the initial solution.
I didn't need it in my solution, but haven't investigated where exactly the issue comes from, yet.

Seems like the original solution was automaticly ported to a new GHC version, and that broke it. The code compiles fine with NoPolyKinds language extension set, so i propose enabling it

My solution passes sample tests, but fails to compile on submission

test/ImperativeSpec.hs:216:1: error:
    • Uninferrable type variable k10 in
      the type synonym right-hand side:
      forall v st (s :: k10).
      HasValue st v b =>
      Var st a -> v -> Imperative @{k10} @{k10} st s s ()
    • In the type declaration for ‘Op’
    |
216 | type Op a b = forall v st s. HasValue st v b => Var st a -> v -> Imperative st s s ()
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Idk, it looks like an internal problem

Hmmm, you're right. Apparently, I didn't check the initial solution before posting this. I've encountered that error because I added an export list (probably copied it from sample tests' imports). Export lists play nicely with IDEs. For instance, they allow me to "rename symbol" in VSCode. I suggest adding one

The initial solution exports everything, so that isn't a problem, is it?

In case anyone is interested in creating another follow-up imperative kata, it would be cool to require correct early returns:

testReturnFromBlock :: String
testReturnFromBlock = def do
  if' 1 (==) 1 do
    early <- var "correct early return"
    return early
  late <- var "incorrect late return"
  return late

Just an observation: default signatures like

var :: a -> Imperative st s s (Var st a)
while :: (HasValue st v a, HasValue st w b) => v -> (a -> b -> Bool) -> w -> Imperative st s t r -> Imperative st s s ()

return an Imperative … s s …, which allows
putting these statements between if', elif' and else':

-- Note how far apart are if' and else'.
example :: String
example = def do
    result <- var "value doesn't matter"
    if' 0 (==) 0 do
        result .= "body doesn't matter"
    varBetween <- var "value doesn't matter"
    while 0 (/=) 0 do
        result .= "body doesn't matter"
    else' do
        result .= "body doesn't matter"
    return result

I'd prefer if this was illegal
and the types of non-branching statements
were restricted to Imperative … s NothingYet …,
given the kata's focus on type correctness.

But sure, this can be seen as an intentional language feature.
And things will probably stay the same
to avoid extra work, breaking existing solutions, etc.
You may even add tests that cover this feature.

Submission tests expect HasValue, Imperative and Var to be exported. Consider adding these to the export list in the initial solution template

I think that error message is a result of UndecidableInstances masking the real problem. Without that option, GHC throws an error, that it can not see, that the functional dependency t → r is satisfied in the second instance:

    • Illegal instance declaration for ‘Variadic a r (a' -> t)’
        The coverage condition fails in class ‘Variadic’
          for functional dependency: ‘t -> r’
        Reason: lhs type ‘a' -> t’ does not determine rhs type ‘r’
        Un-determined variable: r
        Using UndecidableInstances might help
    • In the instance declaration for ‘Variadic a r (a' -> t)’
   |
13 | instance (a ~ a', Variadic a r t) => Variadic a r (a' -> t) where
   |  

Removing the functional dependency resolves that, but then GHC complains about an ambiguous type in polyList.
I have no idea how to resolve that. I have been banging my head against the wall for a whole day trying to get a similar solution working, before settling for a less elegant solution.

Thanks for the feedback!
I added these clarifications to the initial code for .= and toString.

The meaning of the (.=) operation should be clarified (in the initial code comments). It took me some time to realized that it is an assignment operation.

Also, I suggest to clarify that toString is supposed to work with variables only (otherwise it is necessary to use another GHC extension to type check it).

This solution breaks on GHC 9.0, which is unfortunate because I really like it.

Even after reading the migration guide I have no clue what causes the issue in this case. Does someone know how to fix this solution on GHC 9.0+?

• Couldn't match type ‘Int -> Int’ with ‘Int’
    arising from a functional dependency between:
      constraint ‘Variadic Int Int (Int -> Int)’
        arising from a use of ‘polyAdd’
      instance ‘Variadic a r r’
        at oneFunctionManyArguments.hs:14:10-23
• In the expression: polyAdd 1
  In an equation for ‘a’: a = polyAdd 1

It looks very similar to the range function from python to me (excluding the step = 0 case).
So I don't think it is that strange to want such behavior.

# python 3
>>> list(range(10))
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
>>> list(range(5, 10))
[5, 6, 7, 8, 9]
>>> list(range(5, 10, 2))
[5, 7, 9]
>>> list(range(10, 5))
[]

This is a cool kata! I found a two points of frustrations, though.

1. There are no tests for the individual operators. Finding out what exactly went wrong on these big programs is annoying.
2. Not all operators are actually tested/needed. You can get a shorter solution if you simply ignore the untested operators.