Почему «нейтральный» не нормализуется до «[]» в моноиде списка?

Question

Следующие проверки типов определения Idris с помощью Idris 1.3.0:

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

однако это не так:

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

дает следующую ошибку типа:

 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

Почему neutral <+> xs здесь не нормализуется до xs?

Answer 1

neutral будет интерпретироваться как неявный аргумент, потому что он в нижнем регистре и появляется в объявлении типа.Но вы можете просто указать модуль.:doc neutral дает мне Prelude.Algebra.neutral:

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