Agda-2.3.2.2: test/fail/NaturalAndLevelDifferent.agda

module NaturalAndLevelDifferent where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN LEVEL   ℕ #-}