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 |