Bug when using refinements to define an inductive type

[andricicezar]

This fails:

noeq                                                                                                                                                                                    
type rtyp : Type0 -> Type u#1 =
| RR : #s:Type0 -> p:(s → Type0) ->rtyp (x:s{p x})

but this works fine:

let test (s:Type0) (p:s -> Type0) : Type0 = x:s{p x}

noeq
type rtyp : Type0 -> Type u#1 =
| RR : #s:Type0 -> p:(s -> Type0) -> rtyp (test s p)                                                                                                                                                           

The error message is not that informative, and I also don't know exactly why it fails.

[mtzguido]

What is failing to typecheck is the projector for p, I think due to #1948 (since just giving a name to the refinement makes it work, by avoiding the hash consing).

You can add [@@no_auto_projectors] to this declaration to avoid generating the automatic projectors, and this works. You can define the projectors if needed.

We also have a tactic that should make these things work out of the box (Tactics.MkProjectors, see also #3382). But deploying it everywhere without breaking stuff has proven very hard.