[GHC] #14991: GHC HEAD regression involving TYPEs in type families

#14991: GHC HEAD regression involving TYPEs in type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This program typechecks on GHC 8.2.2 and 8.4.1: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind type family Promote (k :: Type) :: Type type family PromoteX (a :: k) :: Promote k type family Demote (k :: Type) :: Type type family DemoteX (a :: k) :: Demote k ----- -- Type ----- type instance Demote Type = Type type instance Promote Type = Type type instance DemoteX (a :: Type) = Demote a type instance PromoteX (a :: Type) = Promote a ----- -- Arrows ----- data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type instance Demote (a ~> b) = DemoteX a -> DemoteX b type instance Promote (a -> b) = PromoteX a ~> PromoteX b }}} However, it fails to typecheck on GHC HEAD: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:34:34: error: • Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’ • In the first argument of ‘(~>)’, namely ‘PromoteX a’ In the type ‘PromoteX a ~> PromoteX b’ In the type instance declaration for ‘Promote’ | 34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b | ^^^^^^^^^^ Bug.hs:34:48: error: • Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’ • In the second argument of ‘(~>)’, namely ‘PromoteX b’ In the type ‘PromoteX a ~> PromoteX b’ In the type instance declaration for ‘Promote’ | 34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b | ^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14991 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14991: GHC HEAD regression involving TYPEs in type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is conceivably correct behavior. In the last two lines, all we know about the kinds of `a` and `b` is that they are `TYPE r1` and `TYPE r2`. Because you don't have instances to promote/demote `TYPE`, GHC gets stuck. In function type signatures, GHC defaults `RuntimeRep`s to `LiftedRep`. Perhaps it should, also, in type family instances. I don't know why this behavior changed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14991#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14991: GHC HEAD regression involving TYPEs in type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (`Track type variable scope more carefully.`) is responsible. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14991#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14991: GHC HEAD regression involving TYPEs in type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: (none) => goldfire -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14991#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14991: GHC HEAD regression involving TYPEs in type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * priority: normal => high -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14991#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14991: GHC HEAD regression involving TYPEs in type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I figured this one out. It turns out that `solveEqualities` needs to use `simpl_top`. In my recent patch, I thought I could get away with `solveWanteds`, and no test cases told me I couldn't. Easy enough to fix. Validating now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14991#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14991: GHC HEAD regression involving TYPEs in type families
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: goldfire
Type: bug | Status: new
Priority: high | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.5
checker) | Keywords: TypeInType,
Resolution: | TypeFamilies
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#14991: GHC HEAD regression involving TYPEs in type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T14991 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * testcase: => dependent/should_compile/T14991 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14991#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC