[Agda] termination & open public

[Noam Zeilberger]

Is this a bug?  It seems that definitions exported by "open M public"
are not available to the termination checker.  Here is an example,
which is intended to capture some reasoning about the well-foundedness
of a subformula relationship:
=====
module Main where

  module Formula where
    data Form1 : Set where
      NAT : Form1
      D : Form1 -> Form1

  module Formula' where
    open Formula public

  module Subformula where
    open Formula'

    data Form2 : Set where
      OBU : Form2
      E : Form2 -> Form2

    data opt (A : Set) : Set where
      Some : A -> opt A
      None : opt A

    data Foo1 : opt Form1 -> Form1 -> Set where
      Fu : {A : Form1} -> Foo1 (Some A) (D A)
      Fz : Foo1 None NAT
      Fs : {x : opt Form1} -> Foo1 x NAT -> Foo1 x NAT

    data Foo2 : opt Form2 -> Form2 -> Set where
      Gu : {A : Form2} -> Foo2 (Some A) (E A)
      Gz : Foo2 None OBU
      Gs : {x : opt Form2} -> Foo2 x OBU -> Foo2 x OBU

    data _<<1_ : Form1 -> Form1 -> Set where
      1< : {A B : Form1} -> Foo1 (Some A) B -> A <<1 B

    data _<<2_ : Form2 -> Form2 -> Set where
      2< : {A B : Form2} -> Foo2 (Some A) B -> A <<2 B

    data Access1 (f : Form1) : Set where
      Acc1 : ({f' : Form1} -> (f' <<1 f) -> Access1 f') -> Access1 f

    data Access2 (f : Form2) : Set where
      Acc2 : ({f' : Form2} -> (f' <<2 f) -> Access2 f') -> Access2 f

    wfacc1 : (A : Form1) -> {B : Form1} -> (B <<1 A) -> Access1 B
    wfacc1 (D B) (1< Fu) = Acc1 (wfacc1 B)
    wfacc1 NAT (1< (Fs p)) = wfacc1 NAT (1< p)

    wfacc2 : (A : Form2) -> {B : Form2} -> (B <<2 A) -> Access2 B
    wfacc2 (E B) (2< Gu) = Acc2 (wfacc2 B)
    wfacc2 OBU (2< (Gs p)) = wfacc2 OBU (2< p)
=====

Form1 and Form2 are equivalent definitions of formulas, except that
Form2 is defined inside Subformula, while Form1 is exported from
Formula'.  All the other definitions are also alpha-equivalent.  Both
wfacc1 and wfacc2 should be well-founded by the lexicographic ordering
on their two arguments -- however, only wfacc2 passes the termination
checker.  Looking at the output of "agda -v 10", I think that the
termination checker is claiming ignorance about the first argument of
wfacc1.

Noam