[GHC] #13643: Core lint error with TypeInType and TypeFamilyDependencies

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple InjectiveFamilies, TypeInType | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: 12102 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In the code {{{#!hs {-# Language TypeFamilyDependencies #-} {-# Language RankNTypes #-} {-# Language KindSignatures #-} {-# Language DataKinds #-} {-# Language TypeInType #-} {-# Language GADTs #-} import Data.Kind (Type) data Code = I type family Interp (a :: Code) = (res :: Type) | res -> a where Interp I = Bool data T :: forall a. Interp a -> Type where MkNat :: T False instance Show (T a) where show _ = "MkNat" main = do print MkNat }}} but add `{-# Options_GHC -dcore-lint #-}` and we get the attached log from running `runghc /tmp/tPb2.hs > /tmp/tPb2.log`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13643 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | InjectiveFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: 12102 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * Attachment "tPb2.log" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13643 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | InjectiveFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12102 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * related: 12102 => #12102 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13643#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | InjectiveFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12102 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I believe this is the same as #12919, although the symptoms are markedly different. The problem is that (because flattened types have flattened kinds), flattening `T I (False |> co)` (where `co :: Bool ~ Interp I`) yields the ill-kinded `T I False`. Instead, we should change the kind invariant on flattening to say that flattening does not change a type's kind. Then this problem (and #12919) are fixed. I hope. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13643#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | InjectiveFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12102 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): With HEAD I get {{{ <no location info>: warning: In the expression: $fShowT @ 'I @ 'False Kinds don't match in type application: Type variable: a2_a18K :: Interp 'I Arg type: 'False :: Bool Linted Arg kind: Bool <no location info>: warning: In the type ‘Show (T 'I 'False)’ Kind application error in type ‘T 'I 'False’ Function kind = forall (a :: Code). Interp a -> * Arg kinds = [('I, Code), ('False, Bool)] <no location info>: warning: [RHS of $dShow_a18r :: Show (T 'I ('False |> Sym (D:R:Interp[0])))] Kind application error in coercion ‘(T <'I>_N (Sym (Coh (Sym (Coh <'False>_N (Trans (Sym (D:R:Interp[0])) (D:R:Interp[0])))) (Sym (D:R:Interp[0])))))_N’ Function kind = forall (a :: Code). Interp a -> * Arg kinds = [('I, Code), ('False, Bool)] }}} Look at at the type in the second error: {{{ In the type ‘Show (T 'I 'False)’ }}} It's ill-kinded! I discussed with Richard and this is just another example of #12919. Consider what happens if we flatten {{{ T 'I ('False |> g) }}} we'll get the flattened type {{{ T 'I 'False }}} (plus a coercion), which is ill-kinded. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13643#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | InjectiveFamilies, 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 goldfire): * related: #12102 => Comment: #12102 is unrelated, I think. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13643#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | InjectiveFamilies, 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 int-index): * cc: int-index (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13643#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13643: Core lint error with TypeInType and TypeFamilyDependencies
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: | Keywords:
| InjectiveFamilies, 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 Richard Eisenberg

#13643: Core lint error with TypeInType and TypeFamilyDependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: | InjectiveFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T13643 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => typecheck/should_compile/T13643 * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13643#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC