1{-# LANGUAGE PatternSynonyms #-}
2{-# LANGUAGE RankNTypes #-}
3{-# LANGUAGE ViewPatterns #-}
4{-# LANGUAGE TypeOperators #-}
5{-# LANGUAGE DataKinds #-}
6module T403 where
7
8pattern (:&&:) :: () =>           ((k :+ 1) ~ n) => a -> HoHeList k a -> HoHeList n a
9pattern ((:&&:))xrest <- (matchNext -> Right (x, Refl, rest))
10
11