I also thought they would be stricter.

I liked that they weren't, which meant I had to create extra type families and thus I learnt a lot more about the pattern, buuuuuut... if this were marked in the description somehow, I'd have scored a victory on first pass, which is always nice (and the amount of times you do this is tallied in your profile!)

So... more information, pwetty please? :3

Fixed ;-)

I hope you mean 'semantically correct' ...

Well, I did told you to reuse the combinators to prevent expanding into SK hell ;-)

As mentioned in the comments at the beginning of part 4, that type should really be something like forall a. Bool a, but it's not possible to encode that type there, and lambda calculus Booleans require a more expressive system then STLC (e.g System F) to encode.

So you just need to write something that's semantically correct, which then you can either remove that type annotation, or change it to something that matches your correct type.

Incidentally, you can even write not' with a type of SKI (Bool' (Bool' a) -> Bool' a) instead of SKI (Bool' a -> Bool' a) and get a lambda term that's completely correct.

The comparison is done recursively.

A more appropriate wording would be select the one with the largest width of the first element of the array in which they differ :)

Did you also follow the order in which the pieces should be cut and ordered?

See the question I raised below :)

Done.

Actually the test case is something like

solve [[False]] (0, 0) (0, 0)

So Nothing is expected.
I didn't mention this in the description, I'll add it now.
Thx for feedback

wait

No answer so resolved.

Alright, feel free to reopen the issue, in case it happens again.

Could you please specify in more detail? I can't find one.

Corrected! I changed the description... but not that part. Marked as resolved if you consider it is. Thanks for the feedback!