Admin message

Due to a large amount of spam we do not allow new users to create repositories, they are "external" users. If you are a new user and want to create a repository, for example for forking GHC, open a new issue on ghc/ghc using the "get-verified" issue template

Ordering of declarations can cause typechecking to fail
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. <details><summary>Trac metadata</summary> | Trac field | Value | | ---------------------- | ----------------------- | | Version | 8.2.1 | | Type | Bug | | TypeOfFailure | OtherFailure | | Priority | normal | | Resolution | Unresolved | | Component | Compiler (Type checker) | | Test case | | | Differential revisions | | | BlockedBy | | | Related | | | Blocking | | | CC | | | Operating system | | | Architecture | | </details> <!-- {"blocked_by":[],"summary":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n-- data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n |\r\n23 | type F' CInst (b :: F CInst) = G b\r\n | \r\n}}}\r\n\r\nHowever, 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`.\r\n\r\nThis 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).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} -->
issue