Serokell’s Work on GHC: Dependent Types, Part 5

• The flip situation is indeed rather disappointing. For reference, Agda’s type for flip looks like this:

  flip : ∀ {A : Set a} {B : Set b} {C : A → B → Set c} →
         ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
  flip f = λ y x → f x y
  

And it relies on higher-order unification to instantiate C at use sites. It’s not clear to me what the Haskell solution to this problem could be.

• The ExplicitNamespaces problem is easier to address. Making one extension imply another is a one-line change, from the implementation standpoint.