[GHC] #8109: Type family patterns should support as-patterns.

1 Aug 2013

      #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

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)