Opened 3 months ago

Closed 3 months ago

#14991 closed bug (fixed)

GHC HEAD regression involving TYPEs in type families

Reported by: RyanGlScott Owned by: goldfire
Priority: high Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: TypeInType, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: dependent/should_compile/T14991
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This program typechecks on GHC 8.2.2 and 8.4.1:

{-# 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
   |                                                ^^^^^^^^^^

Change History (7)

comment:1 Changed 3 months ago 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 RuntimeReps to LiftedRep. Perhaps it should, also, in type family instances.

I don't know why this behavior changed.

comment:2 Changed 3 months ago by RyanGlScott

Commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (Track type variable scope more carefully.) is responsible.

comment:3 Changed 3 months ago by simonpj

Owner: set to goldfire

comment:4 Changed 3 months ago by RyanGlScott

Priority: normalhigh

comment:5 Changed 3 months ago 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.

comment:6 Changed 3 months ago by Richard Eisenberg <rae@…>

In d8d4266b/ghc:

Fix #14991.

It turns out that solveEqualities really does need to use simpl_top.
I thought that solveWanteds would be enough, and no existing test
case showed up the different. #14991 shows that we need simpl_top.
Easy enough to fix.

test case: dependent/should_compile/T14991

comment:7 Changed 3 months ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: dependent/should_compile/T14991
Note: See TracTickets for help on using tickets.