Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,323
    • Issues 4,323
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 385
    • Merge Requests 385
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #8109

Closed
Open
Opened Aug 01, 2013 by carlhowells@trac-carlhowells

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
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#8109