Re: [GHC] #10806: Type error and type level (<=) together cause GHC to hang

28 Aug 2015

      #10806: Type error and type level (<=) together cause GHC to hang
-------------------------------------+-------------------------------------
        Reporter:  htebalaka         |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler (Type    |                 Version:  7.10.2
  checker)                           |
      Resolution:                    |                Keywords:
Operating System:  MacOS X           |            Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Other             |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by htebalaka:

Old description:
...
The following incorrect type in the function wrongArity triggers an
infinite loop in GHC, though only in the presence of triggersLoop. 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.
{{{#!hs
{-# 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
wrongArity :: a -> a
wrongArity _ a = a
triggersLoop :: Q b -> Q b -> Bool
triggersLoop (Q _ _) (Q _ _) = undefined
}}}
New description:

 The following incorrect type in the function wrongArity triggers an
 infinite loop at compile time, though only in the presence of
 triggersLoop. 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.
 {{{#!hs

 {-# 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

 wrongArity :: a -> a
 wrongArity _ a = a

 triggersLoop :: Q b -> Q b -> Bool
 triggersLoop (Q _ _) (Q _ _) = undefined
 }}}

--

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10806#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler