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,400
    • Issues 5,400
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 588
    • Merge requests 588
  • 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
  • #14164
Closed
Open
Issue created Aug 28, 2017 by Icelandjack@IcelandjackReporter

GHC hangs on type family dependency

{-# Language TypeOperators, DataKinds, PolyKinds, KindSignatures, TypeInType, GADTs, TypeFamilyDependencies #-}

import Data.Kind

type Cat a = a -> a -> Type

data SubList :: Cat [a] where
  SubNil :: SubList '[] '[]
  Keep   :: SubList xs ys -> SubList (x:xs) (x:ys)
  Drop   :: SubList xs ys -> SubList xs     (x:ys)

type family 
  UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a]) | res -> pf ys' xs where
  UpdateWith '[]    '[]    SubNil      = '[]
  UpdateWith (y:ys) '[]    SubNil      = y:ys
  -- UpdateWith '[]    (_:_)  (Keep _)    = '[]
  UpdateWith (y:ys) (_:xs) (Keep rest) = y:UpdateWith ys xs rest
  -- UpdateWith ys     (x:xs) (Drop rest) = x:UpdateWith ys xs rest

seems to loop forever on the "Renamer/typechecker"

$ ghci -ignore-dot-ghci -v /tmp/u.hs 
GHCi, version 8.3.20170605: http://www.haskell.org/ghc/  :? for help
Glasgow Haskell Compiler, Version 8.3.20170605, stage 2 booted by GHC version 8.0.2

[...]

*** Parser [Main]:
!!! Parser [Main]: finished in 1.31 milliseconds, allocated 0.651 megabytes
*** Renamer/typechecker [Main]:

[hangs]

while

type family 
  UpdateWith (ys'::[a]) (xs::[a]) (pf::SubList ys xs) = (res :: [a]) | res -> pf ys' xs where
  UpdateWith '[]    '[]    SubNil      = '[]
  UpdateWith (y:ys) '[]    SubNil      = y:ys
  UpdateWith '[]    (_:_)  (Keep _)    = '[]

immediately gives

$ ghc -ignore-dot-ghci /tmp/u.hs 
[1 of 1] Compiling Main             ( /tmp/u.hs, /tmp/u.o )

/tmp/u.hs:14:3: error:
    • Type family equations violate injectivity annotation:
        UpdateWith '[] '[] 'SubNil = '[] -- Defined at /tmp/u.hs:14:3
        forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).
          UpdateWith '[] (_2 : _1) ('Keep _3) = '[]
            -- Defined at /tmp/u.hs:16:3
    • In the equations for closed type family ‘UpdateWith’
      In the type family declaration for ‘UpdateWith’
   |
14 |   UpdateWith '[]    '[]    SubNil      = '[]
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

/tmp/u.hs:16:3: error:
    • Type family equation violates injectivity annotation.
      Type and kind variables ‘_2’, ‘_1’, ‘xs’, ‘_3’
      cannot be inferred from the right-hand side.
      Use -fprint-explicit-kinds to see the kind arguments
      In the type family equation:
        forall a (xs :: [a]) (_1 :: [a]) (_2 :: a) (_3 :: SubList xs _1).
          UpdateWith '[] (_2 : _1) ('Keep _3) = '[]
            -- Defined at /tmp/u.hs:16:3
    • In the equations for closed type family ‘UpdateWith’
      In the type family declaration for ‘UpdateWith’
   |
16 |   UpdateWith '[]    (_:_)  (Keep _)    = '[]
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Trac metadata
Trac field Value
Version 8.2.1
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
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