> On May 24, 2018, at 8:21 AM, Joachim Breitner <mail at joachim-breitner.de> wrote: > > Which one is it? See Note [The substitution invariant] in TyCoRep. That applies to types, not terms, but I'd be shocked if terms had a different situation. That would suggest that the answer is (A) (and that the WARNing is correct). Richard