[GHC] #10507: Looping with type level naturals

10 Jun 2015

      #10507: Looping with type level naturals
-------------------------------------+-------------------------------------
              Reporter:  jhendrix    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
              Keywords:              |  Operating System:  MacOS X
          Architecture:  x86_64      |   Type of failure:  GHC rejects
  (amd64)                            |  valid program
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 When compiling the code below, I run into an error with GHC 7.10.1:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE ExplicitNamespaces #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeOperators #-}
 module Loop ( ) where

 import Data.Type.Equality ( (:~:)(Refl) )
 import Prelude (Maybe(..), undefined)
 import GHC.TypeLits ( Nat, type (<=))

 data V (n::Nat)

 testEq :: (m <= n) => V m -> V n -> Maybe (m :~: n)
 testEq = undefined

 uext :: (1 <= m, m <= n) => V m -> V n -> V n
 uext e w =
   case testEq e w of
     Just Refl -> e
 }}}

 The error I get in GHC 7.10.1 is:
 {{{#!hs
 % ghc -c Loop.hs

 Loop.hs:21:9:
     Context reduction stack overflow; size = 102
     Use -fcontext-stack=N to increase stack size to N
       (1 GHC.TypeLits.<=? n) ~ 'GHC.Types.True
 }}}

 GHC 7.8.4 compiles this without errors.

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