Beta reduction not happening in the presence of coercions (?)

roboguy13 commented 7 years ago

I have part of an expression that looks like this in HERMIT pretty-printed Core:

(λ x f g → g x) b

If I try to beta reduce this, however, HERMIT says that this is not in the appropriate form.

Setting it to show coercions, I have this

((λ x f g → g x)
   ▹ (ForAllCo b
        (refl)
        (ForAllCo a
           (refl)(refl → (sym (axiomInst N:Iter 0 refl refl)))))) b

and if I further enable detailed type information I see this

((λ (b ∷ *) (a ∷ *) (x ∷ b) (r ∷ *) (f ∷ ForAllTy Anon a
                                           (r)) (g ∷ ForAllTy Anon b
                                                       (r)) →
    g x)
   ▹ (ForAllCo b
        (<N:*>)
        (ForAllCo a
           (<N:*>)(<R:b> → (sym (axiomInst N:Iter 0 <R:a> <R:b>)))))) Int (Int, Int, Int) b

I'm not sure if this reduction is fundamentally unsound, or if this is enough information to determine what's going on, but I thought I'd ask just in case something about this pops out.

roboguy13 commented 7 years ago

It occurs to me that Iter is a newtype for a function type, which is probably relevant here (and probably where the coercions are coming from).

xich commented 7 years ago

Yeah, the rightward triangle is a cast (casts are pairs of expression and coercion that proves the cast is type-safe). There should be a cast-float-app rewrite:

https://github.com/ku-fpg/hermit/blob/master/src/HERMIT/Dictionary/Local/Cast.hs#L40

(there are a few other rewrites for casts in that module, but we really have nothing systematic. Finding a paper or description of coercions in GHC and fleshing out an algebra for moving them around would be a super valuable addition for working with real code in HERMIT)

And yes, newtypes become casts in Core. Type functions and GADTs are the other two big sources.

ku-fpg / hermit

Beta reduction not happening in the presence of coercions (?) #183