Opened 17 months ago

# Strange/bad error message binding unboxed type variable

Reported by: Owned by: dfeuer normal 8.2.3 Compiler (Type checker) 8.3 TypeInType goldfire Unknown/Multiple Unknown/Multiple None/Unknown

### 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#))’


### comment:2 follow-up:  3 Changed 17 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 17 months ago by dfeuer

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 15 months ago by bgamari

Milestone: 8.2.2 → 8.2.3

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

### comment:5 Changed 5 months 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 months 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 follow-up:  8 Changed 5 months 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 months ago by RyanGlScott

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 months 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
; 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.