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

[GHC]

#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