idris-0.99.2: test/regression001/reg003.idr
data Point : Num t => Nat -> t -> Type where
Nil : Point Z t
data Mono : (Monoid m) => () -> Type where
Monono : (Monoid m) => Mono {m} ()
data Mono1 : (Monoid m) => Type where
Monono1 : (Monoid m) => Mono1 {m}
data Mono2 : (m : Type) -> Monoid m => () -> Type where
Monono2 : (Monoid m) => Mono2 m ()