Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,252
    • Issues 5,252
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 561
    • Merge requests 561
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #16436
Closed
Open
Issue created Mar 14, 2019 by Vladislav Zavialov@int-indexDeveloper

Pattern matching breaks injective type families

{-# LANGUAGE TypeFamilyDependencies, TypeOperators, DataKinds, GADTs, TypeApplications #-}

data HList xs where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x:xs)

type family ListId xs = ys | ys -> xs
  where
    ListId '[] = '[]
    ListId (x:xs) = (x : ListId xs)

f :: HList (ListId ts) -> ()
f a =
  case a of
    HNil -> ()
--  z@(HCons _ _) -> f z   -- uncomment to break
    z -> f z

While z -> f z works, pattern matching on HCons breaks it:

A.hs:16:24: error:
    • Could not deduce: ListId xs ~ xs1
      from the context: ListId ts ~ (x : xs1)
        bound by a pattern with constructor:
                   HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
                 in a case alternative
        at A.hs:16:8-16
      ‘xs1’ is a rigid type variable bound by
        a pattern with constructor:
          HCons :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs),
        in a case alternative
        at A.hs:16:8-16
      Expected type: HList (ListId (x : xs))
        Actual type: HList (ListId ts)
    • In the first argument of ‘f’, namely ‘z’
      In the expression: f z
      In a case alternative: z@(HCons _ _) -> f z
   |
16 |     z@(HCons _ _) -> f z
   |                        ^
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking