Idris 1中如何拼接String类型字符串与Char类型字符？

报错根因 #

这是Idris 1 REPL中:let命令的类型推导机制特性导致的问题，两个报错的逻辑关联如下：

• 第一个Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Data.Vect.::报错：你编写的[e2]集合字面量，Idris 1无法自动推导具体的集合类型，pack函数虽然要求入参为List Char，但REPL的类型推导顺序会先校验集合字面量的构造器，还没关联到pack的参数类型约束就触发了多构造器歧义。
• 第二个No type declaration for e3是推导失败后的连锁报错：你虽然为e3写了String类型标注，但Idris 1的:let命令对绑定变量的类型标注解析优先级低于右侧表达式的推导，表达式推导失败后就会抛出找不到类型声明的错误。

可用解决方案 #

三种写法都可以正常实现String和Char的拼接：

1. 给列表字面量加显式类型标注，明确指定集合为List类型：

:let e3 : String = e1 ++ pack (the (List Char) [e2])

2. 用Prelude内置的singleton函数把Char直接转成单字符String后拼接，写法更简洁：

:let e3 : String = e1 ++ singleton e2

3. 拆分e3的类型声明和赋值步骤，先给REPL明确变量类型再绑定值：

:let e3 : String
:let e3 = e1 ++ pack [e2]

注：该推导歧义问题在Idris 2中已经做了优化，不需要额外标注即可正常识别pack入参的List类型。

内容的提问来源于stack exchange，提问作者Ashwin