
#8109: Type family patterns should support as-patterns. ------------------------------------+------------------------------------- Reporter: carlhowells | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- I recently wrote code similar to the following: {{{ {-# LANGUAGE DataKinds, ScopedTypeVariables, TypeOperators, TypeFamilies #-} {-# LANGUAGE PolyKinds, FlexibleInstances, FlexibleContexts #-} import GHC.TypeLits data P n = P fromNat :: forall (p :: Nat -> *) (n :: Nat). SingI n => p n -> Integer fromNat _ = fromSing (sing :: Sing n) class C (a :: [Nat]) where type T a :: * val :: p a -> T a instance SingI n => C '[n] where type T '[n] = Integer val _ = fromNat (P :: P n) instance (SingI n, C (n2 ': ns)) => C (n ': n2 ': ns) where type T (n ': n2 ': ns) = (Integer, T (n2 ': ns)) val _ = (fromNat (P :: P n), val (P :: P (n2 ': ns))) }}} There were semantic constraints in my case that made an empty list nonsensical, so it wasn't an appropriate base case. But the resulting effort in ensuring type family patterns didn't overlap got unwieldy. I would have much preferred to write that second instance more like this: {{{ instance (SingI n, C ns) => C (n ': ns@(_ ': _)) where type T (n ': ns) = (Integer, T ns) val _ = (fromNat (P :: P n), val (P :: P ns)) }}} The reasoning here is identical to as-patterns in value-level pattern matching. If you only want to match an expression when it has a particular sub-structure, it's way more convenient to do it with an as-pattern. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8109 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler