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.