#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