Opened 2 years ago
Last modified 8 months 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 (10)
comment:1 Changed 2 years ago by
Cc: | goldfire added |
---|
comment:2 follow-up: 3 Changed 2 years ago by
comment:3 Changed 2 years ago by
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 23 months ago by
Milestone: | 8.2.2 → 8.2.3 |
---|
It looks like this won't be fixed for 8.2.2.
comment:5 Changed 13 months ago by
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 13 months ago by
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 13 months ago by
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 Changed 13 months ago by
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 13 months ago by
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.
comment:10 Changed 8 months ago by
To motivate why I want this, it's because the kind-generics library (described in the paper Generics of All Kinds) is attempting to come up with a uniform representation of both lifted and unlifted types. Due to the way kind-generics
works, we need to implement a type family with this shape:
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
Where k
is the type of the type being interpreted. At the moment, since k :: Type
, Interpret
is exclusively limited to use with lifted types. I'd like to be able to instead say:
type family Interpret (t :: Atom d (k :: TYPE r)) (tys :: LoT d) :: (k :: TYPE r) where
But GHC won't let me do so for the same reasons as in this ticket.
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.