13-patfun-target.egi

--
-- Pattern function target side (PAT-APP's target half).  `seqp` produces
-- a Pattern [Tile], but the matcher and target are [Integer].  Before the
-- PAT-APP fix this silently failed at runtime.
--
-- Expected: Type error (Tile vs Integer)
--

inductive Tile := Num Integer | Hnr Integer
inductive pattern Tile := num Integer | hnr Integer

def pattern seqp (pat1: Tile) (pat2: [Tile]) : [Tile] :=
  (num $n & ~pat1) :: num #(n + 1) :: ~pat2

def t := matchAll [1, 2] as multiset integer with seqp #(Num 1) _ -> True