Tyxml should not accept a form as an indirect descendant of another form

[darioteixeira]

Tyxml's phantom-type trickery prevents a form from being the child of another form:

# Html5.M.(form [form []]);;
Error: This expression has type ([> Html5_types.form ] as 'a) Html5.M.elt
       but an expression was expected of type
         ([< Html5_types.form_content_fun ] as 'b) Html5.M.elt

However, it does not prevent a form from being the grandchild of another form:

# Html5.M.(form [div [form []]]);;
- : [> Html5_types.form ] Html5.M.elt = <abstr>

There seems to be at least one example in the wild where this loophole caused problems: depending on the content-type, browsers will either reluctantly accept nested forms or reject them by messing with the parse tree.

This problem is probably difficult to fix without major changes to Tyxml's phantom-type trickery, but should perhaps be at least documented, as it's damn hard to diagnose when things go wrong.

[Drup]

(I'm happy, this is the first time someone complains about tyxml not being strict enough :p)

This may be solvable (changing the type machinery can be done in a backward compatible fashion), but certainly not in the short term. There is mecanism to ensure this kind of nesting property for a, so we should be able to do it.

[shepard8]

Hello,

I was about to open a new issue, but I think it is related to this one.

The @Drup comment indicates that the content model of the a element should be enforced by TyXML. That is, no interactive element such as "a" should be a descendent of any "a" element.

However the following will compile:

open Tyxml
let _ = Html.a [Html.span [Html.a []]]

As far as I understand TyXML, the problem comes from the fact that types phrasing_without_interactive and flow5_without_interactive both contain `Span and not `Span of X_without_interactive (where X is phrasing or flow5, respectively), and likewise for other elements.

[Drup]

@shepard8 Important thing to note is that "a inside a" is only forbidden lazily. a [a []] is fine, body [a [a []]] is not. That being said, yes, it looks like there is a typing issue with "forbidden grand children".

[calimeroteknik]

Using the same concepts as TyXML to generate valid documents via type enforcement, this potential issue came to mind, and I couldn't think of a strategy to handle it.

@Drup you mentioned it was doable, so I grew curious. By what mechanism would this be made possible at an arbitrary depth?

[Drup]

@calimeroteknik the trick is to use type parameters to track a bit precisely what was inside. For instance, the type of Html.a can be summarize as 'a elt list -> (`A 'a) elt. Then, you can encode an automaton in the types (which is what tyxml does), to ensure that an `A never comes after another `A.

Currently, in tyxml, most of the types are simple (for instance, span is more or less phrasing elt list -> phrasing elt). We could apply the same treatment here, and parameterize everything. This is a bit annoying because it makes all the check delayed and the types more complicated.