Agda-2.3.2.2: test/fail/Imports/Test.agda
{-# OPTIONS --universe-polymorphism #-}
module Imports.Test where
open import Imports.Level
record Foo (ℓ : Level) : Set ℓ where
{-# OPTIONS --universe-polymorphism #-}
module Imports.Test where
open import Imports.Level
record Foo (ℓ : Level) : Set ℓ where