Opened 2 years ago

Closed 2 years ago

#13788 closed bug (invalid)

TypeInType fails to compile old code

Reported by: br1 Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1-rc2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-#  LANGUAGE TypeInType              #-}

module PP where

newtype Field l v   =   Field { value :: v }

label  ::  Field l v -> l
label  =   undefined

class HEq x
hEq :: HEq x => x -> Int
hEq = undefined

class HListGet r where
    hListGet :: r -> Int
instance
    HEq l => HListGet (Field l v) where
    hListGet f = hEq (label f)

fails with

mini.hs:18:29: error:
    • Couldn't match type ‘k’ with ‘*’
      ‘k’ is a rigid type variable bound by
        the instance declaration at mini.hs:17:5-33
      Expected type: Field * l v
        Actual type: Field k l v
    • In the first argument of ‘label’, namely ‘f’
      In the first argument of ‘hEq’, namely ‘(label f)’
      In the expression: hEq (label f)
    • Relevant bindings include
        f :: Field k l v (bound at mini.hs:18:14)
        hListGet :: Field k l v -> Int (bound at mini.hs:18:5)
   |
18 |     hListGet f = hEq (label f)
   |

Change History (4)

comment:1 Changed 2 years ago by goldfire

This looks like correct behavior to me. With -XTypeInType, GHC will generalize kinds, including the kind of HEq (now forall k. k -> Constraint) and of Field (now forall k. k -> Type -> Type). However, label can't be generalized; it has type forall (l :: Type) (v :: Type). Field @Type l v -> l. (I'm using @ to denote a normally-elided parameter.)

Because the instance at the end doesn't constraint the kind of l, the type of f is Field @k l v, where k is implicitly bound in the instance declaration. Accordingly, it can't be passed to label.

The solution: add a kind signature: instance HEq l => HListGet (Field (l :: Type) v) where .... (You will have to import Type from Data.Kind.)

Please close the ticket if you agree with my analysis. Thanks!

comment:2 Changed 2 years ago by br1

Your solution works. The problem is that adding TypeInType requires adding kind signatures all over. Then TypeInType is not an extension but a breaking change.

comment:3 Changed 2 years ago by goldfire

This isn't an issue with TypeInType, per se, but with PolyKinds, which originally added kind generalization. (You'll find that compiling with just PolyKinds causes the same effect as you're observing with TypeInType.)

Many of the language "extensions" have the potential to break code. For example, OverloadedStrings can cause declarations like x = length "hi" to fail, because GHC can no longer tell what type "hi" should be.

comment:4 Changed 2 years ago by br1

Resolution: invalid
Status: newclosed

I see now. Thanks!

Note: See TracTickets for help on using tickets.