Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Register
  • Sign in
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
    • Locked files
  • Issues 5.5k
    • Issues 5.5k
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 637
    • Merge requests 637
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • Analytics
    • Analytics
    • 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
  • #16512

Type-checker loop involving injective type families

I ran into a type-checking loop with GHC 8.6.4 while working on pattern synonyms for function applications within the context of a typed AST.
The issue seems to be with injective type families (nothing to do with pattern synonyms); I boiled it down to the following program (with a few comments left in for context):

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE ViewPatterns           #-}

import Data.Kind
  ( Type )

-- HOAS representation
data AST (a :: Type) :: Type where  
  (:$) :: AST ( a -> b ) -> AST a -> AST b
  -- Lam :: ( AST a -> AST b ) -> AST ( a -> b )
  -- PrimOp :: PrimOp op a => AST a
  -- ...

data ASTs (as :: [Type]) :: Type where
  NilASTs :: ASTs '[]
  ConsAST :: AST a -> ASTs as -> ASTs (a ': as)

type family ListVariadic (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where  
  ListVariadic (a ': as) b = a -> ListVariadic as b
  -- ListVariadic '[] ()     = ()
  -- ListVariadic '[] Bool   = Bool
  -- ListVariadic '[] Word   = Word 
  -- ListVariadic '[] Int    = Int
  -- ListVariadic '[] Float  = Float
  -- ListVariadic '[] Double = Double
  -- ...

data AnApplication b where
  AnApplication :: AST (ListVariadic as b) -> ASTs as -> AnApplication b

unapply :: AST b -> AnApplication b
unapply (f :$ a)
  = case unapply f of
        AnApplication g as -> 
          AnApplication g (a `ConsAST` as)
-- no other cases with this simplified AST

On GHC 8.6.4, attempting to compile this program seems to send the type-checker in a loop, consuming more and more memory (GHC consumed up to 6GB of RAM before I closed it).
Removing the injectivity annotation on ListVariadic fixes this, and produces the expected error

  Couldn't match type ‘ListVariadic as (a -> b)’ with ‘a -> ListVariadic as b’
      Expected type: AST (ListVariadic (a : as) b)
        Actual type: AST (ListVariadic as (a -> b))

The correct code is instead

unapply :: AST b -> AnApplication b
unapply (f :$ a)
  = case unapply f of
        AnApplication g as -> 
          AnApplication g (as `snocAST` as)

where snocAST is as you'd expect. This is pretty much working as I want (module some difficulties with injective type-level Snoc and type inference, but nevermind), so the bug is not causing me any trouble at the moment.

By the way, if anyone knows of a better way to provide an injectivity annotation for ListVariadic which avoids this messy approach of explicitly listing non-function-types that are going to be used, I'd be interested. It somehow amounts to providing evidence to GHC that a type variable cannot be instantiated to a function type (in this situation the constraint ListVariadic '[] a ~ a kind of fills this role but is still quite limited). I asked a question about this with slightly more context on stackoverflow.

I wasn't able to add any labels to this ticket to help categorising it, sorry.

Edited Mar 31, 2019 by sheaf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking