CODEWITHSUNDEEP
typeclassidristype-level-computation
Cactus
Cactus

Reputation: 27626

Why does 'neutral' not normalize to '[]' in the List monoid?

The following Idris definition typechecks with Idris 1.3.0:

foo : (xs : List Nat) -> xs = ([] <+> xs)
foo xs = Refl

however, this doesn't:

foo : (xs : List Nat) -> xs = (neutral <+> xs)
foo xs = Refl

giving the following type error:

 When checking right hand side of foo with expected type
         xs = neutral <+> xs

 Type mismatch between
         neutral ++ xs = neutral ++ xs (Type of Refl)
 and
         xs = neutral ++ xs (Expected type)

 Specifically:
         Type mismatch between
                 neutral ++ xs
         and
                 xs

Why does neutral <+> xs not normalize to xs here?

Upvotes: 0

Views: 60

Answers (1)

xash
xash

Reputation: 3722

neutral will be interpreted as a implicit argument because it's lower case and appears in a type declaration. But you can just specify the module. :doc neutral gives me Prelude.Algebra.neutral:

foo : (xs : List Nat) -> xs = (Algebra.neutral <+> xs)
foo xs = Refl

Upvotes: 1

Related Questions