Specializing the universally quantified types of a binding

[roboguy13]

We have inst-lemma for instantiating universally quantified variables of a lemma, but is there an equivalent for instantiating type variables of a binding?

The particular issue I'm running into is that, for examples/fib-stream, the wrap and unwrap functions have a more general type than is required:

wrap :: Stream a -> (Nat -> a)
wrap s n = s !! n

unwrap :: (Nat -> a) -> Stream a
unwrap f = map f nats

as a result, when I try to run ww-split-unsafe [| wrap |] [| unwrap |] I get

Rewrite failed:given expressions have the wrong types to form a valid wrap/unwrap pair.

The system doesn't seem to accept ww-split-unsafe [| wrap Nat |] [| unwrap Nat |] either, giving the error:

Rewrite failed:Nat lookup: Variable not in scope.

I could circumvent this by giving monomorphic types for these functions, but I was wondering if there is a way to keep the more general types.

[xich]

The issue is that the type check for the ww-split rewrites is somewhat simple... it doesn't try to unify, and just checks for equality, which will fail because the two universally quantified as will have different uniques.

We really need to convert this example to use the new W/W infrastructure (split-1-beta, split-2-beta, etc) and deprecate all the old W/W stuff (anything not in HERMIT.Dictionary.WorkerWrapper itself).

Also, is Nat a type synonym? Have you tried using the underlying type instead?

[roboguy13]

Nat isn't a type synonym:

data Nat = Zero | Succ Nat deriving (Eq,Show)

For the time being, I just monomorphized the as in the signatures to Nat.