Skip to content

Type error and type level (<=) together cause GHC to hang

The following incorrect arity triggers an infinite loop at compile time. The issue is somehow related to the use of (<=) in constraints of the Q data constructor; if I remove either of the constraints or add an (a <= c) constraint it works as you would expect.

{-# LANGUAGE GADTs, ExplicitNamespaces, TypeOperators, DataKinds  #-}

import GHC.TypeLits (Nat, type (<=))

data Q a where
    Q :: (a <= b, b <= c) => proxy a -> proxy b -> Q c

triggersLoop :: Q b -> Q b -> Bool
triggersLoop (Q _ _) (Q _ _) = print 'x' 'y'

Incorrect function definitions, like foo :: a -> a ; foo _ x = x also result in an infinite loop.

Edited by htebalaka
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information