[GHC] #13035: GHC enters a loop when partial type signatures and advanced type level code mix

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC loops when compiling this code. Replacing the _ with the actual type fixes the error. {{{#!hs {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, TypeFamilies, TemplateHaskell, GADTs, PartialTypeSignatures #-} import Data.Vinyl import Data.Singletons.TH newtype MyAttr a b = MyAttr { _unMyAttr :: MyFun (a b) } type MyRec a b = Rec (MyAttr a) b type family MyFun (a :: k1) :: k2 data GY (a :: k1) (b :: k2) (c :: k1 -> k3) (d :: k1) data GNone (a :: k1) type family GYTF a where GYTF (GY a b _ a) = b GYTF (GY _ _ c d) = MyFun (c d) type instance MyFun (GY a b c d) = GYTF (GY a b c d) type family GNoneTF (a :: k1) :: k2 where type instance MyFun (GNone a) = GNoneTF a type (a :: k1) =: (b :: k2) = a `GY` b type (a :: j1 -> j2) $ (b :: j1) = a b infixr 0 $ infixr 9 =: data FConst (a :: *) (b :: Fields) data FApply (a :: * -> * -> *) b c (d :: Fields) data FMap (a :: * -> *) b (d :: Fields) type instance MyFun (FConst a b) = a type instance MyFun (FApply b c d a) = b (MyFun (c a)) (MyFun (d a)) type instance MyFun (FMap b c a) = b (MyFun (c a)) data Fields = Name | Author | Image | Description | Ingredients | Instructions | CookTime | PrepTime | TotalTime | Yield | Nutrition | Tags | Url | Section | Items | Subsections | Calories | Carbohydrates | Cholesterol | Fat | Fiber | Protien | SaturatedFat | Sodium | Sugar | TransFat | UnsaturatedFat | ServingSize genSingletons [ ''Fields ] (=::) :: sing f -> MyFun (a f) -> MyAttr a f _ =:: x = MyAttr x type NutritionT = Calories =: Maybe Int $ Carbohydrates =: Maybe Int $ Cholesterol =: Maybe Int $ Fat =: Maybe Int $ Fiber =: Maybe Int $ Protien =: Maybe Int $ SaturatedFat =: Maybe Int $ Sodium =: Maybe Int $ Sugar =: Maybe Int $ TransFat =: Maybe Int $ UnsaturatedFat =: Maybe Int $ ServingSize =: String $ GNone type NutritionRec = MyRec NutritionT ['Calories, 'Carbohydrates, 'Cholesterol, 'Fat, 'Fiber, 'Protien, 'SaturatedFat, 'Sodium, 'Sugar, 'TransFat, 'UnsaturatedFat, 'ServingSize] type RecipeT = Name =: String $ Author =: String $ Image =: String $ Description =: String $ CookTime =: Maybe Int $ PrepTime =: Maybe Int $ TotalTime =: Maybe Int $ Yield =: String $ Nutrition =: NutritionRec $ Tags =: [String] $ Url =: String $ GNone type RecipeFormatter = FApply (->) (FConst [String]) (FMap IO RecipeT) g :: MyRec RecipeFormatter _ --'[ 'Author ] Uncomment to prevent loop g = SAuthor =:: (\a -> return "Hi") :& RNil main = putStrLn "Hi" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here is a version which doesn't have any dependencies on `singletons` or `vinyl`: {{{#!hs {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, TypeFamilies, GADTs, PartialTypeSignatures #-} newtype MyAttr a b = MyAttr { _unMyAttr :: MyFun (a b) } type MyRec a b = Rec (MyAttr a) b type family MyFun (a :: k1) :: k2 data GY (a :: k1) (b :: k2) (c :: k1 -> k3) (d :: k1) data GNone (a :: k1) type family GYTF a where GYTF (GY a b _ a) = b GYTF (GY _ _ c d) = MyFun (c d) type instance MyFun (GY a b c d) = GYTF (GY a b c d) type family GNoneTF (a :: k1) :: k2 where type instance MyFun (GNone a) = GNoneTF a type (a :: k1) =: (b :: k2) = a `GY` b type (a :: j1 -> j2) $ (b :: j1) = a b infixr 0 $ infixr 9 =: data FConst (a :: *) (b :: Fields) data FApply (a :: * -> * -> *) b c (d :: Fields) data FMap (a :: * -> *) b (d :: Fields) type instance MyFun (FConst a b) = a type instance MyFun (FApply b c d a) = b (MyFun (c a)) (MyFun (d a)) type instance MyFun (FMap b c a) = b (MyFun (c a)) data Fields = Name | Author | Image | Description | Ingredients | Instructions | CookTime | PrepTime | TotalTime | Yield | Nutrition | Tags | Url | Section | Items | Subsections | Calories | Carbohydrates | Cholesterol | Fat | Fiber | Protien | SaturatedFat | Sodium | Sugar | TransFat | UnsaturatedFat | ServingSize data Rec :: (u -> *) -> [u] -> * where RNil :: Rec f '[] (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs) data family Sing (a :: k) data instance Sing (z_a6bn :: Fields) = z_a6bn ~ Name => SName | z_a6bn ~ Author => SAuthor | z_a6bn ~ Image => SImage | z_a6bn ~ Description => SDescription | z_a6bn ~ Ingredients => SIngredients | z_a6bn ~ Instructions => SInstructions | z_a6bn ~ CookTime => SCookTime | z_a6bn ~ PrepTime => SPrepTime | z_a6bn ~ TotalTime => STotalTime | z_a6bn ~ Yield => SYield | z_a6bn ~ Nutrition => SNutrition | z_a6bn ~ Tags => STags | z_a6bn ~ Url => SUrl | z_a6bn ~ Section => SSection | z_a6bn ~ Items => SItems | z_a6bn ~ Subsections => SSubsections | z_a6bn ~ Calories => SCalories | z_a6bn ~ Carbohydrates => SCarbohydrates | z_a6bn ~ Cholesterol => SCholesterol | z_a6bn ~ Fat => SFat | z_a6bn ~ Fiber => SFiber | z_a6bn ~ Protien => SProtien | z_a6bn ~ SaturatedFat => SSaturatedFat | z_a6bn ~ Sodium => SSodium | z_a6bn ~ Sugar => SSugar | z_a6bn ~ TransFat => STransFat | z_a6bn ~ UnsaturatedFat => SUnsaturatedFat | z_a6bn ~ ServingSize => SServingSize (=::) :: sing f -> MyFun (a f) -> MyAttr a f _ =:: x = MyAttr x type NutritionT = Calories =: Maybe Int $ Carbohydrates =: Maybe Int $ Cholesterol =: Maybe Int $ Fat =: Maybe Int $ Fiber =: Maybe Int $ Protien =: Maybe Int $ SaturatedFat =: Maybe Int $ Sodium =: Maybe Int $ Sugar =: Maybe Int $ TransFat =: Maybe Int $ UnsaturatedFat =: Maybe Int $ ServingSize =: String $ GNone type NutritionRec = MyRec NutritionT ['Calories, 'Carbohydrates, 'Cholesterol, 'Fat, 'Fiber, 'Protien, 'SaturatedFat, 'Sodium, 'Sugar, 'TransFat, 'UnsaturatedFat, 'ServingSize] type RecipeT = Name =: String $ Author =: String $ Image =: String $ Description =: String $ CookTime =: Maybe Int $ PrepTime =: Maybe Int $ TotalTime =: Maybe Int $ Yield =: String $ Nutrition =: NutritionRec $ Tags =: [String] $ Url =: String $ GNone type RecipeFormatter = FApply (->) (FConst [String]) (FMap IO RecipeT) g :: MyRec RecipeFormatter _ --'[ 'Author ] Uncomment to prevent loop g = SAuthor =:: (\a -> return "Hi") :& RNil main = putStrLn "Hi" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): FWIW, I don't think this is causing the typechecker to loop, but rather it causes it to take an extremely long time to complete. I discovered this by trying to minimize the test case by commenting some lines in the definition of `RecipeT`: {{{#!hs type RecipeT = Name =: String $ Author =: String {- $ Image =: String $ Description =: String $ CookTime =: Maybe Int $ PrepTime =: Maybe Int $ TotalTime =: Maybe Int $ Yield =: String -} $ Nutrition =: NutritionRec {- $ Tags =: [String] $ Url =: String -} $ GNone }}} When I compiled this, it lagged noticeably, but it completed in finite time: {{{ $ time /opt/ghc/8.0.1/bin/ghc -fforce-recomp Wat.hs[1 of 1] Compiling Wat ( Wat.hs, Wat.o ) Wat.hs:140:28: warning: [-Wpartial-type-signatures] • Found type wildcard ‘_’ standing for ‘'['Author]’ • In the type signature: g :: MyRec RecipeFormatter _ • Relevant bindings include g :: MyRec RecipeFormatter '['Author] (bound at Wat.hs:141:1) real 0m1.973s user 0m1.940s sys 0m0.028s }}} I then uncommented one more line (`Image := String`): {{{#!hs type RecipeT = Name =: String $ Author =: String $ Image =: String {- $ Description =: String $ CookTime =: Maybe Int $ PrepTime =: Maybe Int $ TotalTime =: Maybe Int $ Yield =: String -} $ Nutrition =: NutritionRec {- $ Tags =: [String] $ Url =: String -} $ GNone }}} And that contributed to the compilation time significantly (almost doubling it): {{{ $ time /opt/ghc/8.0.1/bin/ghc -fforce-recomp Wat.hs[1 of 1] Compiling Wat ( Wat.hs, Wat.o ) Wat.hs:140:28: warning: [-Wpartial-type-signatures] • Found type wildcard ‘_’ standing for ‘'['Author]’ • In the type signature: g :: MyRec RecipeFormatter _ • Relevant bindings include g :: MyRec RecipeFormatter '['Author] (bound at Wat.hs:141:1) real 0m3.635s user 0m3.564s sys 0m0.068s }}} Similarly, uncommented out more and more lines seems to approximately double the compilation time for each line. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): According to a profiled build of GHC HEAD, `TcRnDriver.tc_rn_src_decls` is taking up almost 100% of the time and alloc when compiling the program above. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by xcmw): For some reason this similar code works fine. The only change I made was creating and using NutritionW. {{{ {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, TypeFamilies, GADTs, PartialTypeSignatures, UndecidableInstances #-} newtype MyAttr a b = MyAttr { _unMyAttr :: MyFun (a b) } type MyRec a b = Rec (MyAttr a) b type family MyFun (a :: k1) :: k2 data GY (a :: k1) (b :: k2) (c :: k1 -> k3) (d :: k1) data GNone (a :: k1) type family GYTF a where GYTF (GY a b _ a) = b GYTF (GY _ _ c d) = MyFun (c d) type instance MyFun (GY a b c d) = GYTF (GY a b c d) type family GNoneTF (a :: k1) :: k2 where type instance MyFun (GNone a) = GNoneTF a type (a :: k1) =: (b :: k2) = a `GY` b type (a :: j1 -> j2) $ (b :: j1) = a b infixr 0 $ infixr 9 =: data FConst (a :: *) (b :: Fields) data FApply (a :: * -> * -> *) b c (d :: Fields) data FMap (a :: * -> *) b (d :: Fields) type instance MyFun (FConst a b) = a type instance MyFun (FApply b c d a) = b (MyFun (c a)) (MyFun (d a)) type instance MyFun (FMap b c a) = b (MyFun (c a)) data Fields = Name | Author | Image | Description | Ingredients | Instructions | CookTime | PrepTime | TotalTime | Yield | Nutrition | Tags | Url | Section | Items | Subsections | Calories | Carbohydrates | Cholesterol | Fat | Fiber | Protien | SaturatedFat | Sodium | Sugar | TransFat | UnsaturatedFat | ServingSize data Rec :: (u -> *) -> [u] -> * where RNil :: Rec f '[] (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs) data family Sing (a :: k) data instance Sing (z_a6bn :: Fields) = z_a6bn ~ Name => SName | z_a6bn ~ Author => SAuthor | z_a6bn ~ Image => SImage | z_a6bn ~ Description => SDescription | z_a6bn ~ Ingredients => SIngredients | z_a6bn ~ Instructions => SInstructions | z_a6bn ~ CookTime => SCookTime | z_a6bn ~ PrepTime => SPrepTime | z_a6bn ~ TotalTime => STotalTime | z_a6bn ~ Yield => SYield | z_a6bn ~ Nutrition => SNutrition | z_a6bn ~ Tags => STags | z_a6bn ~ Url => SUrl | z_a6bn ~ Section => SSection | z_a6bn ~ Items => SItems | z_a6bn ~ Subsections => SSubsections | z_a6bn ~ Calories => SCalories | z_a6bn ~ Carbohydrates => SCarbohydrates | z_a6bn ~ Cholesterol => SCholesterol | z_a6bn ~ Fat => SFat | z_a6bn ~ Fiber => SFiber | z_a6bn ~ Protien => SProtien | z_a6bn ~ SaturatedFat => SSaturatedFat | z_a6bn ~ Sodium => SSodium | z_a6bn ~ Sugar => SSugar | z_a6bn ~ TransFat => STransFat | z_a6bn ~ UnsaturatedFat => SUnsaturatedFat | z_a6bn ~ ServingSize => SServingSize (=::) :: sing f -> MyFun (a f) -> MyAttr a f _ =:: x = MyAttr x type NutritionT = Calories =: Maybe Int $ Carbohydrates =: Maybe Int $ Cholesterol =: Maybe Int $ Fat =: Maybe Int $ Fiber =: Maybe Int $ Protien =: Maybe Int $ SaturatedFat =: Maybe Int $ Sodium =: Maybe Int $ Sugar =: Maybe Int $ TransFat =: Maybe Int $ UnsaturatedFat =: Maybe Int $ ServingSize =: String $ GNone data NutritionW (x :: Fields) type instance MyFun (NutritionW x) = MyFun (NutritionT x) type NutritionRec = MyRec NutritionW ['Calories, 'Carbohydrates, 'Cholesterol, 'Fat, 'Fiber, 'Protien, 'SaturatedFat, 'Sodium, 'Sugar, 'TransFat, 'UnsaturatedFat, 'ServingSize] type RecipeT = Name =: String $ Author =: String $ Image =: String $ Description =: String $ CookTime =: Maybe Int $ PrepTime =: Maybe Int $ TotalTime =: Maybe Int $ Yield =: String $ Nutrition =: NutritionRec $ Tags =: [String] $ Url =: String $ GNone type RecipeFormatter = FApply (->) (FConst [String]) (FMap IO RecipeT) g :: MyRec RecipeFormatter _ --'[ 'Author ] Uncomment to prevent loop g = SAuthor =:: (\a -> return "Hi") :& RNil main = putStrLn "Hi" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13035: GHC enters a loop when partial type signatures and advanced type level code
mix
-------------------------------------+-------------------------------------
Reporter: xcmw | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.3 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | perf/compiler/T13035 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => perf/compiler/T13035 * milestone: => 8.0.3 Comment: Thanks for a great report. It compiles in a flash now. Merge to 8.0.3 if convenient. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.3 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | perf/compiler/T13035 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Phyx-): The test for this commit seems to currently be failing on all platforms https://phabricator.haskell.org/harbormaster/build/17689/ -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.3 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | perf/compiler/T13035 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I believe mpickering fixed in in f3c7cf9b89cad7f326682b23d9f3908ebf0f8f9d and 54227a45352903e951b81153f798162264f02ad9. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13035: GHC enters a loop when partial type signatures and advanced type level code mix -------------------------------------+------------------------------------- Reporter: xcmw | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.3 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | perf/compiler/T13035 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes I forgot to add a file; my fault. Thanks to Matthew for adding it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13035#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC