An example of some confusing highlighting when using HoTT-Agda.

Hmm.agda

{-# OPTIONS --without-K #-}

{-
 Load this file as-is, and Agda will highlight the S m == S n term, and complain:

Sort _4  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:43,27-37 ]
_A_6 : Set _4  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:43,31-33 ]
_8 : _A_6  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:43,27-30 ]
_10 : _A_6  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:43,34-37 ]
_11 : _8 == _10  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:44,10-13 ]
_12 : _8 == _10  [ at /Users/allan.erskine/Dev/HoTT-Exercises/Hmm.agda:44,10-13 ]

However, if the import lines 5 - 6 are then commented out and replaced with the directly-copied
code from the HoTT-Agda lib, then everything works fine (no highlighting, no complaints).
-}

module Hmm where

open import lib.Base
open import lib.types.Nat

-- postulate  -- Universe levels
--   ULevel : Set
--   lzero : ULevel
--   lsucc : ULevel → ULevel
--   lmax : ULevel → ULevel → ULevel

-- {-# BUILTIN LEVEL ULevel #-}
-- {-# BUILTIN LEVELZERO lzero #-}
-- {-# BUILTIN LEVELSUC lsucc #-}
-- {-# BUILTIN LEVELMAX lmax #-}

-- Type : (i : ULevel) → Set (lsucc i)
-- Type i = Set i

-- Type₀ = Type lzero
-- Type0 = Type lzero

-- Type₁ = Type (lsucc lzero)
-- Type1 = Type (lsucc lzero)

-- data ℕ : Type₀ where
--   O : ℕ
--   S : (n : ℕ) → ℕ

-- {-# BUILTIN NATURAL ℕ #-}
-- {-# BUILTIN ZERO O #-}
-- {-# BUILTIN SUC S #-}

-- infix 3 _==_

-- data _==_ {i} {A : Type i} (a : A) : A → Type i where
--   idp : a == a

-- Path = _==_

S= : {m n : ℕ} → m == n → S m == S n
S= idp = idp