packages feed

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