egison-5.1.0: test/type-error/50-matcher-collection-hetero.egi
--
-- Heterogeneous matcher collection (matcher rigidity). Putting `something :
-- Matcher b` and `list integer : Matcher [Integer]` in one list would unify
-- b with [Integer], giving `something` a matcher type whose structural
-- capability it does not have: binding $m to the first element and using it
-- at a cons pattern would then pass the dual check yet get stuck at runtime.
-- Matcher types are rigid -- their unification is forbidden -- so the list
-- literal itself is rejected.
--
-- Expected: Type error (matcher types are rigid: Matcher b vs Matcher [Integer])
--
def t := matchAll [something, list integer] as list something with
| $m :: _ ->
matchAll [1, 2] as m with
| $x :: _ -> x