Skip to content

GitLab

  • Menu
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 4,864
    • Issues 4,864
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 452
    • Merge requests 452
  • 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 Compiler
  • GHCGHC
  • Issues
  • #9974
Closed
Open
Created Jan 09, 2015 by David Feuer@treeowlReporter

Allow more general structural recursion without UndecidableInstances

I bet this is a duplicate, but I couldn't find it.

A simple example from the HList package:

{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
type family HRevApp (l1 :: [k]) (l2 :: [k]) :: [k]
type instance HRevApp '[] l = l
type instance HRevApp (e ': l) l' = HRevApp l (e ': l')

GHC 7.8.3 and 7.11 both complain about the second instance if UndecidableInstances is turned off, because the application is no smaller than the index head. Moreover, the same error occurs when the type family is closed. However, GHC already knows how to separate term-level definitions into recursive groups; applying this same analysis to the type family above would reveal that HRevApp is structurally recursive, and therefore decidable. It is key, in this case, that the instance for [] is visible from the instance declaration for e ': l, so such an analysis could only be done in module dependency order for open type families.

Side note: there is a (nasty) workaround available for the problem in this case:

type family HRevApp' (l1 :: [k]) (l1' :: [k])  (l2 :: [k]) :: [k]
type instance HRevApp' t '[] l = l
type instance HRevApp' (e ': l) (e' ': l') l'' = HRevApp' l l' (e ': l'')

type HRevApp l1 l2 = HRevApp' l1 l1 l2
Edited Mar 10, 2019 by Thomas Miedema
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking