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
Cc: | goldfire added |
---|
comment:2 follow-up: 3 Changed 13 months ago by
comment:3 Changed 13 months 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 11 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 5 weeks 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 5 weeks 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 5 weeks 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 5 weeks 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 5 weeks 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.
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.