GitLab

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.