destrNF produces ill-typed terms

This is not an issue for now since we don't really rely on types anywhere on the translation, but it's worth documenting and leaving the issue open.

The problem: the Pirouette.Term.Transformation.destrNF pushes a function down the branches of a destructor: Say t = [f [d/Maybe x N (\ J)] a0 a1], where f is not a destructor, it returns:

[d/Maybe x [f N a0 a1] (\ [f J a0 a1])]

That's all fine until we have to deal with types. The last statements of destrNF say:

      guard (not $ isDest f)
      ...
      (tyN, tyArgs, x, ret, cases) <- unDest dest
      ...
      return $ R.App (R.F (FreeName (DestOf tyN)))
             $ map R.TyArg tyArgs ++ [R.Arg x, R.TyArg ret] ++ map R.Arg cases'
      --                                               ^^^
      --                                                 Should not be ret, but the result type of f

Taking our example above, let x : Maybe a, N : T and J : a -> T for some types a and T, the result of unDest would be something like: tyN == Maybe, tyArgs == a, x == x, ret == T, cases == [N, J], yet, say f : T -> U, the resulting destructor will have result type U but we're constructing it with resulting type T anyway.

Fixing this is harder than it sounds, since we would need to be able to get the type of an arbitrary f at any point in the transformation pipeline. This actually seems reasonable as we should construct a PirouetteM monad with logging and environment information which should enable us to quickly compute the correct resulting type.

I will leave this for a future re-implementation of the prototype or until we start using types to direct the translation.

tweag / pirouette

destrNF produces ill-typed terms #2