Opened 6 years ago

Last modified 9 months ago

#8109 new feature request

Type family patterns should support as-patterns.

Reported by: carlhowells Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: newcomer, TypeFamilies Cc: vogt.adam@…, ThrashAbaddon
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (9)

comment:1 Changed 6 years ago by aavogt

Cc: vogt.adam@… added

comment:2 Changed 5 years ago by goldfire

See also example at #9608, which is a duplicate of this ticket.

comment:3 Changed 5 years ago by jstolarek

Keywords: newcomer added

comment:4 Changed 4 years ago by qnikst

Owner: set to qnikst

comment:5 Changed 4 years ago by thomie

qnikst: any progress? Please ask if you need help with anything, or unassign yourself if you don't plan to work on this ticket anymore.

comment:6 Changed 4 years ago by qnikst

@thomie, still working I'm planning to invest more time into this ticket after this weekend.

comment:7 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:8 Changed 9 months ago by ThrashAbaddon

Cc: ThrashAbaddon added

comment:9 Changed 9 months ago by qnikst

Owner: qnikst deleted

Seems, I have neither a good understanding on how to implement this ticket, nor enough time to pass through all changes in the parser and further, so if anyone would like to solve this one - feel free to.

Note: See TracTickets for help on using tickets.