type 'a n = [ Z of 'a | S of 'a n ].
type t = [ N of t n ].
Type t is empty but EC loops indefinitely while evaluating its definition. Indeed the current implementation of the emptiness test
eagerly evaluates any type constructor by instantiating its type parameters and processing recursively, which may cause a cyclic behaviour:
|
and isempty_dtype (targs, tname) = |
|
if EcPath.p_equal tname tpath then true else |
|
|
|
let tdecl = EcEnv.Ty.by_path_opt tname env0 |
|
|> odfl (EcDecl.abs_tydecl ~params:(`Named tparams) lc) in |
|
let tyinst = ty_instantiate tdecl.tyd_params targs in |
|
|
|
match tdecl.tyd_type with |
|
| Abstract -> |
|
List.exists isempty targs |
|
|
|
| Concrete ty -> |
|
isempty_1 [ tyinst ty ] |
|
|
|
| Record (_, fields) -> |
|
isempty_1 (List.map (tyinst -| snd) fields) |
|
|
|
| Datatype dt -> |
|
(* FIXME: Inspecting all constructors recursively causes |
|
non-termination in some cases. One can have the same |
|
limitation as is done for positivity in order to limit this |
|
unfolding to well-behaved cases. *) |
|
isempty_n (List.map (List.map tyinst -| snd) dt.tydt_ctors) |
