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,407
    • Issues 5,407
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 603
    • Merge requests 603
  • 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
  • #2219
Closed
Open
Issue created Apr 14, 2008 by dolio@trac-dolio

GADT match fails to refine type variable

The following code is accepted by the type checker in 6.8.2, but is rejected by a HEAD build, 6.9.20080411:

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

data Zero
data Succ a

data FZ
data FS fn

data Fin n fn where
  FZ :: Fin (Succ n) FZ
  FS :: Fin n fn -> Fin (Succ n) (FS fn)

data Nil
data a ::: b

type family Lookup ts fn :: *
type instance Lookup (t ::: ts) FZ = t
type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn

data Tuple n ts where
  Nil   :: Tuple Zero Nil
  (:::) :: t -> Tuple n ts -> Tuple (Succ n) (t ::: ts)

proj :: Fin n fn -> Tuple n ts -> Lookup ts fn
proj FZ      (v ::: _)  = v
proj (FS fn) (_ ::: vs) = proj fn vs

The error in question is:

Bug.hs:25:16:
    Occurs check: cannot construct the infinite type:
      t = Lookup (t ::: ts) fn
    In the pattern: v ::: _
    In the definition of `proj': proj FZ (v ::: _) = v

Which seems to indicate that the pattern match against FZ in the first case is failing to refine the type variable fn to FZ. Reversing the order of the cases yields the same error, so either the match against FS is working correctly, or the type checker thinks that it can solve Lookup (t ::: ts) fn ~ Lookup ts fn.

Trac metadata
Trac field Value
Version 6.9
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
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