Opened 13 months ago

Last modified 5 weeks ago

#14180 new bug

Strange/bad error message binding unboxed type variable

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.2.3
Component: Compiler (Type checker) Version: 8.3
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# language TypeInType, TypeFamilies, MagicHash #-}

import GHC.Exts

type family MatchInt (f :: Int) :: () where
  MatchInt ('I# x) = '()

produces

<interactive>:2:59: error:
    • Couldn't match a lifted type with an unlifted type
      When matching kinds
        k0 :: *
        Int# :: TYPE 'IntRep
      Expected kind ‘Int#’, but ‘x’ has kind ‘k0’
    • In the first argument of ‘ 'I#’, namely ‘x’
      In the first argument of ‘MatchInt’, namely ‘( 'I# x)’
      In the type family declaration for ‘MatchInt’

If, however, I replace x in the pattern with _, the type checker is satisfied. If I give it a pattern signature,

MatchInt ('I# (x :: Int#)) = '()

I get a different (and equally unhelpful) error message,

    • Expecting a lifted type, but ‘Int#’ is unlifted
    • In the kind ‘Int#’
      In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’
      In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’

Change History (9)

comment:1 Changed 13 months ago by dfeuer

Cc: goldfire added

comment:2 Changed 13 months ago by simonpj

What do you expect to happen here? We just don't have unboxed ints at the type level. Doubtless the error message could be improved.

comment:3 in reply to:  2 Changed 13 months ago by dfeuer

Replying to simonpj:

What do you expect to happen here? We just don't have unboxed ints at the type level. Doubtless the error message could be improved.

Well, a message to that effect would be much better than what we get now! But I don't have a sufficiently clear sense of exactly what is and is not allowed to write it myself. Something about variables bound in type families not being able to have kinds of kind TYPE r unless r ~ PtrRepLifted, perhaps?

comment:4 Changed 11 months ago by bgamari

Milestone: 8.2.28.2.3

It looks like this won't be fixed for 8.2.2.

comment:5 Changed 5 weeks ago by RyanGlScott

For what it's worth, the situation here appears to have changed slightly between GHC 8.4.3 and 8.6.1. In 8.4.3, one could work around this issue by replacing the x (in MatchInt ('I# x) = '()) with _. However, this is no longer be the case in 8.6.1, where even replacing x with _ will yield this error:

Bug.hs:6:17: error:
    • Couldn't match a lifted type with an unlifted type
      When matching kinds
        k0 :: *
        Int# :: TYPE 'IntRep
      Expected kind ‘Int#’, but ‘_’ has kind ‘k0’
    • In the first argument of ‘ 'I#’, namely ‘_’
      In the first argument of ‘MatchInt’, namely ‘( 'I# _)’
      In the type family declaration for ‘MatchInt’
  |
6 |   MatchInt ('I# _) = '()
  |                 ^

comment:6 Changed 5 weeks ago by RyanGlScott

As far as why this error even happens in the first place, there appears to be some strangeness in the way the kind of the arrow (->) type constructor is generalized in type families. For example, this does not kind-check:

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import GHC.Exts (Int#, TYPE)

type family F :: Int# -> Int
Bug2.hs:10:18: error:
    • Expecting a lifted type, but ‘Int#’ is unlifted
    • In the kind ‘Int# -> Int’
   |
10 | type family F :: Int# -> Int
   |                  ^^^^

However, one can work around the issue by defining one's own function type:

type Arrow = ((->) :: TYPE p -> TYPE q -> Type)
type family F :: Int# `Arrow` Int

This leads me to wonder: what's the point of not generalizing the kind of (->) to be the same as Arrow, then?

comment:7 Changed 5 weeks ago by simonpj

It's here in tc_fun_type

tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
            -> TcM TcType
tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
  TypeLevel ->
    do { arg_k <- newOpenTypeKind
       ; res_k <- newOpenTypeKind
       ; ty1' <- tc_lhs_type mode ty1 arg_k
       ; ty2' <- tc_lhs_type mode ty2 res_k
       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
                           liftedTypeKind exp_kind }
  KindLevel ->  -- no representation polymorphism in kinds. yet.
    do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
       ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
                           liftedTypeKind exp_kind }

In a kind signature, (mode_level mode) is KindLevel, so we insist that the arguments of (->) are of kind Type.

A type synonym doesn't know what level it is at, so it escapes this check. You are right that this gives silly results.

Now that types and kind are the same, perhaps we shouldn't have this TypeLevel/KindLevel distinction. But I don't know what the raminfications would be, esp for error messages.

Or we could simplfy tc_fun_type to not check the distinction.

But do you really want unboxed types in kinds??

comment:8 in reply to:  7 Changed 5 weeks ago by RyanGlScott

Replying to simonpj:

But do you really want unboxed types in kinds??

...Yes? I mean, that's what dfeuer was presumably trying to do in the original program. But moreover, I find it rather strange that the typing rule for (->) is less general in kinds than it is in types.

I don't care so much about removing the TypeLevel/KindLevel distinction, especially if keeping it will improve error message quality elsewhere. But I do think that we shouldn't check for this distinction in tc_fun_type.

...However, it should be noted that I tried implementing that tc_fun_type suggestion, but even still that doesn't make the original program (the MatchInt one) typecheck, so I guess my hunch was misplaced. For some reason, GHC expects the type of all type variables to have kind Type (as opposed to how things work on the value level, where they can have kind TYPE r for some RuntimeRep r). I'm not sure where that is decided, but it's not tc_fun_type it seems.

comment:9 Changed 5 weeks ago by simonpj

For some reason, GHC expects the type of all type variables to have kind Type

It's here in TcMType:

newMetaKindVar = do { uniq <- newUnique
                    ; details <- newMetaDetails TauTv
                    ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
                    ; traceTc "newMetaKindVar" (ppr kv)
                    ; return (mkTyVarTy kv) }

When we see forall a. blah, we give a the kind \kappa : *. Richard may want to comment on why. It'd be good to add a Note to explain.

Note: See TracTickets for help on using tickets.