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,242
    • Issues 5,242
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 564
    • Merge requests 564
  • 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
  • #12564
Closed
Open
Issue created Sep 02, 2016 by Vladislav Zavialov@int-indexDeveloper

Type family in type pattern kind

I want to write a type family that is analogous to !! for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:

{-# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #-}

import Data.Kind

data N = Z | S N

type family Len (xs :: [a]) :: N where
  Len '[] = Z
  Len (_ ': xs) = S (Len xs)

data Fin :: N -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
  At (x ': _) FZ = x
  At (_ ': xs) (FS i) = At xs i

It fails to compile with this error:

FinAt.hs:16:3: error:
    • Illegal type synonym family application in instance: 'FZ
    • In the equations for closed type family ‘At’
      In the type family declaration for ‘At’

That's because the kind of the FZ pattern (first clause of At) has the kind Fin (Len xs) and the application of Len cannot reduce completely. checkValidTypePat then disallows the pattern, as it contains a type family application.

I tried to suppress checkValidTypePat and the definition of At has compiled; however, it's of little use, since At doesn't reduce:

x :: At '[Bool] FZ
x = True

results in

FinAt.hs:20:5: error:
    • Couldn't match expected type ‘At
                                      * ((':) * Bool ('[] *)) ('FZ 'Z)’
                  with actual type ‘Bool’
    • In the expression: True
      In an equation for ‘x’: x = True
Trac metadata
Trac field Value
Version 8.0.1
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC goldfire, int-index
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking