Sorry! I forgot to reply to this earlier. Here it is now!
Setup
Lets insert an intermediate step quickly:
let paramsPlusLogin = insert (SProxy :: SProxy "login") login (insert (SProxy :: SProxy "passwd") password params)
(insert has a complex type, but let’s not worry about that, since it is already working.)
Now we’re going to look at the last line of the do notation (get (apiUrl <> route) paramsPlusLogin). Let’s set up the local context first – this is one of the most important parts of how compilers work, knowing what is in scope:
| Type Level Variables (and their kinds) |
Value Level Variables (and their types) |
e :: # Type
m :: Type -> Type
p :: # Type
|
route :: ApiRoute
params :: { | p }
login :: String
password :: String
apiUrl :: String
paramsPlusLogin :: { login :: string, passwd :: String | p }
|
And we have some typeclasses constraints, which provide these values:
| Class |
Methods |
MonadJsonHttp e m |
get :: forall p. WriteForeign { | p } => String -> { | p } -> ExceptV e m Json |
MonadApiAccess m |
getApiAccess :: m { login :: String, password :: String, apiUrl :: String } |
Lacks "login" p |
none (but helps with insert) |
| `Lacks “password” p |
none |
WriteForeign { | p } |
writeImpl :: { | p } -> Foreign |
Now our task is to make this line happen:
get (apiUrl <> route) paramsPlusLogin
Now’s where the fun typeclass solving begins!
get :: forall p. WriteForeign { | p } => String -> { | p } and we’re providing it with a string argument (check! 
) and an argument of type { login :: string, passwd :: String | p }. Hmm … that means we need WriteForeign { login :: string, passwd :: String | p }.
Solving for WriteForeign { login :: string, passwd :: String | p }
The compiler maintains a list of instances for each typeclass. A partial list can be found on pursuit for this class: class WriteForeign a.
We notice that there is a instance that pertains to records: instance (RowToList row rl, WriteForeignFields rl row () to) => WriteForeign { | row }. So now we choose row = ( login :: string, passwd :: String | p ) (do you see why?), and continue looking for instances.
In particular, we need both RowToList ( login :: string, passwd :: String | p ) rl and WriteForeignFields rl ( login :: string, passwd :: String | p ) () to, for some unsolved variables rl and to.
Solving RowToList ( login :: string, passwd :: String | p ) rl
Solving RowToList is usually pretty easy, and the compiler does it automatically, generating rl from the row. But this only works for closed rows! It can’t be solved for open rows like ( login :: string, passwd :: String | p ). This is because the RowList needs to be sorted, and you don’t know what the ordering of login and password will be with respect to the rest of p.
Therefore, we cannot reduce this constraint any further, and we have to add the constraint RowToList ( login :: string, passwd :: String | p ) rl to our top-level function. (Or do we?)
This also means that we need to add another type variable to the function too, since rl wasn’t defined. It will have kind RowList.
Solving WriteForeignFields rl ( login :: string, passwd :: String | p ) () to
This class has fundeps rl -> row from to which means that, as rl should be solved by the above, this class should be solvable now.
Unfortunately, we don’t know what rl is, so it can’t be reduced further. This means we again need to add it to the constraints on our function. And add the variable to.
Recap
As noted in the original post, we needed to add these constraints (along with variables rl and x) to let the compiler solve for the correct instance:
⇒ RowToList (login :: String, passwd :: String | p) rl
⇒ WriteForeignFields rl (login :: String, passwd :: String | p) () x
Bu actually, there was another solution too! We could have just added the constraint WriteForeign { login :: String, passwd :: String | p } directly!
What’s the difference? The difference is that the former set of constraints implies the latter one. It’s what the compiler looks for when it needs to solve an instance of WriteForeign for a record type. So having them in scope is sufficient to solve the WriteForeign instance. But it is possible to have it in scope directly too. (Then the caller of the function will end up solving for the sufficient constraints.)
But what about WriteForeign { | p }??
So the interesting thing is that we never mentioned this constraint. It’s actually not necessary!
The deal is, it makes sense conceptually, since solving both constraints requires each of the fields to have a WriteForeign constraint … but it’s not part of how the compiler solves for the WriteForeign { login :: String, passwd :: String | p } instance, so it contributes nothing.
Constraints on rows are complex and tricky; this is not a proof system
In general, that’s the hard part of dealing with rows and rowlists in PureScript. This is because the constraint system is a logical system (it basically models logic), but you can only use the basic inference steps represented by the instances directly. You can’t “prove” any shortcuts.
For instance, it is a true statement that RowCons "sym" t r1 r2 implies Union ( sym :: t ) r1 r2 (in the sense that, in any context t :: Type, r1 :: # Type, r2 :: # Type where the former is solvable, the latter must also be solved). This is essentially how Union works, by iterating over a bunch of RowCons constraints. But that’s not how it is implemented in the compiler, so this argument is not provable.
Or an even simpler example: given an instance for Union r1 r2 (), what do you know about r1 and r2? Well, directly you know that their union is empty … but that must mean they both are empty! However, that again is reasoning that is true, but outside the system of deduction for constraints, as they are solved by the compiler. (This also implies RowLacks sym r1 for any sym, etc.)
Constraint solving algorithm (basics)
The compiler begins by listing all instances that are in scope, in terms of variables and concrete types and whatnot. Then it seeks to match an instance, either directly (e.g. if WriteForeign { login :: String, passwd :: String | p } is in scope, it would use that), or by choosing an instance (which it does based on the fundeps) and continuing to solve the constraints on that instance.
(Of course, this all relies on a notion of unifying types (which assigns type variables to other values, often more concrete, as necessary), and of what types are “apart” and cannot be unified. But those should be pretty intuitive to grasp.)
But notice that it just has one path to go down to solve an instance – if WriteForeign { login :: String, passwd :: String | p } doesn’t exist directly, it’s bound to using the record instance and solving for its constraints instead.
It’s like skiing down a mountain: once you commit to a path, there’s no turning back. Hopefully you don’t hit a dead end 
Follow the instances!
I think that’s the gist of how it works. Maybe others can add to it 
