mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2025-01-08 14:17:43 +03:00
86eb475413
We were only checking parameters, meaning that there were potential clashes leading to confusing behaviour, and meaning that it was somehow relevant what the names were in the interface!
10 lines
303 B
Idris
10 lines
303 B
Idris
interface Foo m where
|
|
bar : k -> v -> m k v -> m k v
|
|
|
|
-- This is kind of meaningless, except it exposes a potential error where
|
|
-- (\s, t => List (s, t)) is substituted in as 'm' in 'm k v' and the ks
|
|
-- clash, so one has to be renamed.
|
|
Eq k => Foo (\s, t => List (s, t)) where
|
|
bar x y z = ?bang
|
|
|