Fix mono matches (1)

[0xd34df00d]

I ended up just replacing any functional type argument to the matcher with the corresponding closure type — those are to be defunctionalized in the match branches anyway.

This doesn't fix all the problems with the ADTs having higher-order fields though. Right now we get the following on the test case:

term Just |->
  Constructor 0 Maybe
term Nothing |->
  Constructor 1 Maybe
term main |->
  Integer
  match_Maybe @Closure!!TyInteger_TyInteger
      val
      @Integer
      (λ f : Closure!!TyInteger_TyInteger . _Apply!!TyInteger_TyInteger 0#f 42)
      0
term match_Maybe |->
  Destructor Maybe
term val |->
  Maybe Integer -> Integer
  Just @(Integer -> Integer) (λ x : Integer . b/add 0#x 1)
type Maybe |->
  Type data a:*
            match_Maybe
            Just : ∀ a : * . 0#a -> (Maybe 0#a)
            Nothing : ∀ a : * . Maybe 0#a

thus we also need to defunctionalize the things around val — the ctor and the type itself.

So far I think it's safe to just blindly replace anything of the form TyCon TyFun{} (where TyCon :: * -> ...) with TyCon ClosureType (where ClosureType corresponds to the TyFun), and similarly with constructors of such TyCons.

I'd be happy to continue hacking on this tomorrow, especially if you agree this is a reasonable thing to do.

Also, our pretty-printer does something funny here, printing Maybe Integer -> Integer. A mental note to self to investigate.

[VictorCMiraldo]

I think that makes sense; if we defunctionalize all constructors that take a function as an argument we should be good! :crossed_fingers:

[0xd34df00d]

Welp, I actually broke the other test (-p '/Defun/ && /Nested/') with the above changes. What gets generated for one of the specializations is

term _Apply!!List<TyInteger>_List<TyInteger>_List<TyInteger> |->
  Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger> -> (List Integer) -> (List Integer) -> (List Integer)
  λ cls : Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger>
  . match_Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger> 0#cls
      @((List Integer) -> (List Integer) -> (List Integer))
      (λ (ctx : AdditiveMonoid!List<TyInteger>) (η : List Integer)
         (η : List Integer) . match_AdditiveMonoid!List<TyInteger> 2#ctx
           @Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger>
           (λ (f : Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger>)
              (z : List Integer) (η : List Integer) (η : List Integer)
            . _Apply!!List<TyInteger>_List<TyInteger>_List<TyInteger> 3#f
                1#η
                0#η)
           1#η
           0#η)
      (λ (ctx : Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger>)
         (ctx : Closure!!List<TyInteger>_List<TyInteger>) (x : List Integer)
         (rest : List Integer)
       . _Apply!!List<TyInteger>_List<TyInteger>_List<TyInteger> 3#ctx
           (_Apply!!List<TyInteger>_List<TyInteger> 2#ctx 1#x)
           0#rest)
      (λ (ctx : Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger>)
         (η : List Integer) (η : List Integer)
       . _Apply!!List<TyInteger>_List<TyInteger>_List<TyInteger> 2#ctx 1#η 0#η)
      (λ (k : List Integer) (l : List Integer)
       . foldr!TyInteger!List<TyInteger> Closure!!TyInteger_List<TyInteger>_List<TyInteger>_ctor_1
           0#l
           1#k)

or, the diff against the good version:

@@ -43,7 +43,7 @@
       @((List Integer) -> (List Integer) -> (List Integer))
       (λ (ctx : AdditiveMonoid!List<TyInteger>) (η : List Integer)
          (η : List Integer) . match_AdditiveMonoid!List<TyInteger> 2#ctx
-           @((List Integer) -> (List Integer) -> (List Integer))
+           @Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger>
            (λ (f : Closure!!List<TyInteger>_List<TyInteger>_List<TyInteger>)
               (z : List Integer) (η : List Integer) (η : List Integer)
             . _Apply!!List<TyInteger>_List<TyInteger>_List<TyInteger> 3#f

I'm over-defunctionalizing here: a functional return type from a match function is OK, I think. It's a trivial fix (defunctionalize only type args until the first term arg, which is what's getting matched), but it makes me think that there are too many ad-hoc special cases in the algorithm, so it'll need to be reworked eventually. Good we have extensive test suite now!

[VictorCMiraldo]

I added one test and updated two tests that show that the monomorphization pass is broken too, types such as:

data Indirect (a : Type)
  = Ind : Maybe (a -> a) -> Indirect a

Are not being scheduled to be monomorphized, even though they must be.