Type family patterns should support as-patterns.

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.

Trac metadata

Trac field	Value
Version	7.6.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture