[GHC] #12522: GHC 8.0.1 hangs, looping forever in type-checker

[GHC]

#12522: GHC 8.0.1 hangs, looping forever in type-checker
-------------------------------------+-------------------------------------
        Reporter:  clinton           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash                              |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by clinton:

@@ -1,2 +1,5 @@
- I'm not sure if this is a bug or hanging the compiler is expected here.
- This was the minimal example that causes GHC to hang:
+ There's a subtle issue going on with injective type families. Simply
+ reordering the arguments can cause an otherwise legal program to hang on
+ compile. Calling `f_bad` instead of `f_good` will cause the compiler to
+ hang, looping forever in the typechecker, but the only difference between
+ `TF_Good` and `TF_Bad` is that the argument order is swapped.
@@ -5,1 +8,1 @@
-     {-# LANGUAGE TypeFamilyDependencies #-}
+ {-# LANGUAGE TypeFamilyDependencies #-}
@@ -7,1 +10,2 @@
-     main = return $ f (Just 'c')
+ main = return $ f_good (Just 'c')
+ --main = return $ f_bad (Just 'c')
@@ -9,2 +13,2 @@
-     data D1 x
-     data D2
+ type family TF x y = t | t -> x y
+ type instance TF Int Float = Char
@@ -12,3 +16,2 @@
-     type family TF x = t | t -> x
-     type instance TF (D1 x, a) = Maybe (TF (x, a))
-     type instance TF (D2, ()) = Char
+ type family TF_Good x y = t | t -> x y
+ type instance TF_Good a (Maybe x) = Maybe (TF a x)
@@ -16,2 +19,8 @@
-     f :: TF (x, a) -> ()
-     f _ = ()
+ f_good :: TF_Good a x -> ()
+ f_good _ = ()
+
+ type family TF_Bad x y = t | t -> x y
+ type instance TF_Bad (Maybe x) a = Maybe (TF a x)
+
+ f_bad :: TF_Bad x a -> ()
+ f_bad _ = ()

New description:

 There's a subtle issue going on with injective type families. Simply
 reordering the arguments can cause an otherwise legal program to hang on
 compile. Calling `f_bad` instead of `f_good` will cause the compiler to
 hang, looping forever in the typechecker, but the only difference between
 `TF_Good` and `TF_Bad` is that the argument order is swapped.

 {{{#!hs
 {-# LANGUAGE TypeFamilyDependencies #-}

 main = return $ f_good (Just 'c')
 --main = return $ f_bad (Just 'c')

 type family TF x y = t | t -> x y
 type instance TF Int Float = Char

 type family TF_Good x y = t | t -> x y
 type instance TF_Good a (Maybe x) = Maybe (TF a x)

 f_good :: TF_Good a x -> ()
 f_good _ = ()

 type family TF_Bad x y = t | t -> x y
 type instance TF_Bad (Maybe x) a = Maybe (TF a x)

 f_bad :: TF_Bad x a -> ()
 f_bad _ = ()
 }}}

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12522#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler