[GHC] #14668: Ordering of declarations can cause typechecking to fail
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | 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: -------------------------------------+------------------------------------- The following will successfully typecheck: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeFamilies #-} data CInst data G (b :: ()) = G class C a where type family F a class (C a) => C' a where type family F' a (b :: F a) -- data CInst instance C CInst where type F CInst = () instance C' CInst where type F' CInst (b :: F CInst) = G b }}} But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: {{{ Test.hs:23:18: error: • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’ • In the second argument of ‘F'’, namely ‘(b :: F CInst)’ In the type instance declaration for ‘F'’ In the instance declaration for ‘C' CInst’ | 23 | type F' CInst (b :: F CInst) = G b | }}} However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`. This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families). I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by heptahedron): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType 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 goldfire): Thanks for the report! The `TypeInType` keyword makes sure it's in my queue. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType 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 simonpj): May, possibly, relate to #12088 or #14451 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType 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 danilo2): Hi! Yet another example which seems related! If you move the data declaration to be the first line, it compiles fine: {{{ {-# LANGUAGE TypeInType #-} module Type.Data.Map where import Prelude import Data.Kind type family KeyKind (obj :: Type) :: Type type family ValKind (obj :: Type) :: Type type family Get (key :: KeyKind a) (obj :: a) :: ValKind a data Map (k :: Type) (v :: Type) = Map [(k,v)] type instance Get k ('Map ('(k,v) ': _)) = v type instance KeyKind (Map k v) = k type instance ValKind (Map k v) = v }}} Otherwise it gives error: {{{ Main.hs:16:19: error: • Occurs check: cannot construct the infinite kind: k0 ~ KeyKind (Map k0 v0) The type variables ‘v0’, ‘k0’ are ambiguous • In the first argument of ‘Get’, namely ‘k’ In the type instance declaration for ‘Get’ | 16 | type instance Get k ('Map ('(k,v) ': _)) = v | ^ Main.hs:16:44: error: • Occurs check: cannot construct the infinite kind: v0 ~ ValKind (Map k0 v0) The type variables ‘k0’, ‘v0’ are ambiguous • In the type ‘v’ In the type instance declaration for ‘Get’ | 16 | type instance Get k ('Map ('(k,v) ': _)) = v }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType 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 danilo2): What is even worse, this bug prevents us from refactoring the code to separate module, so I have to have the `Get` declaration in he same file, under all data definitions that are used to make instances of it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType 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 simonpj):
What is even worse, this bug prevents us from refactoring the code to separate module
That's odd. The original report is about ordering declarations within a single module. Can you give a repro case for how refactoring your code into separate modules makes things fail? Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12088, #12643, | Differential Rev(s): #15561 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #12088, #12643, #15561 Comment: This is almost surely a duplicate of #12088 (see also #12643 and #15561, which are other surely-duplicates of #12088). Here are two tricks to making these sorts of programs compile: 1. `TemplateHaskell`. Using an empty Template Haskell splice can often force GHC's SCC analysis to come to its senses and do the right thing. As an example, the following variations of danilo2's program in comment:4 compiles: {{{#!hs {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Type.Data.Map where import Prelude import Data.Kind type family KeyKind (obj :: Type) :: Type type family ValKind (obj :: Type) :: Type type family Get (key :: KeyKind a) (obj :: a) :: ValKind a data Map (k :: Type) (v :: Type) = Map [(k,v)] type instance KeyKind (Map k v) = k type instance ValKind (Map k v) = v $(pure []) type instance Get k ('Map ('(k,v) ': _)) = v }}} 2. Closed type families. As I discovered recently in #15561, open and closed type families behave differently in SCC analysis, so it turns out that turning `ValKind` into a closed type family makes danilo2's program compile as well: {{{#!hs {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Type.Data.Map where import Prelude import Data.Kind type family KeyKind (obj :: Type) :: Type type family ValKind (obj :: Type) :: Type where ValKind (Map k v) = v type family Get (key :: KeyKind a) (obj :: a) :: ValKind a data Map (k :: Type) (v :: Type) = Map [(k,v)] type instance Get k ('Map ('(k,v) ': _)) = v type instance KeyKind (Map k v) = k }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14668: Ordering of declarations can cause typechecking to fail -------------------------------------+------------------------------------- Reporter: heptahedron | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12088, #12643, | Differential Rev(s): #15561, #15987 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #12088, #12643, #15561 => #12088, #12643, #15561, #15987 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14668#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC