diff options
| author | Pierre-Marie Pédrot | 2019-06-25 13:49:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 13:49:18 +0200 |
| commit | 56488b97395ddf9c9b1b3737a15fcaabf3f8d50a (patch) | |
| tree | 8a0c50afe918418e4a6d15968f017a9c7130c343 | |
| parent | 0c29a6dc3962cf3e6073d9e72a07bf5c279ba0f0 (diff) | |
| parent | d0e258175280152e504a296a05ecbd1920bb17c9 (diff) | |
Merge PR #10162: Fix #10161: occur check when defining an algebraic universe.
Ack-by: SkySkimmer
Ack-by: mattam82
Reviewed-by: ppedrot
| -rw-r--r-- | engine/uState.ml | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_10161.v | 8 |
2 files changed, 10 insertions, 1 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index bd61112f08..5ed016e0d0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -214,7 +214,8 @@ let process_universe_constraints ctx cstrs = | Inr l, Inl r | Inl r, Inr l -> let alg = LSet.mem l ctx.uctx_univ_algebraic in let inst = univ_level_rem l r r in - if alg then (instantiate_variable l inst vars; local) + if alg && not (LSet.mem l (Universe.levels inst)) then + (instantiate_variable l inst vars; local) else let lu = Universe.make l in if univ_level_mem l r then diff --git a/test-suite/bugs/closed/bug_10161.v b/test-suite/bugs/closed/bug_10161.v new file mode 100644 index 0000000000..3d262b89fe --- /dev/null +++ b/test-suite/bugs/closed/bug_10161.v @@ -0,0 +1,8 @@ +Inductive SwitchT (A : Type) : Type := +| switchT : forall T, SwitchT T -> SwitchT A. + +Set Printing Universes. + +Fail Inductive UseSwitchT := +| useSwitchT : SwitchT UseSwitchT -> UseSwitchT. +(* used to stack overflow, should be univ inconsistency cannot satisfy u = u+1 *) |