[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    |           Version:  7.10.2
  (Type checker)                     |
              Keywords:              |  Operating System:  MacOS X
          Architecture:              |   Type of failure:  Other
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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
 }}}

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