[GHC] #14180: Strange/bad error message binding unboxed type variable
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler | Version: 8.3 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# 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, {{{#!hs 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#))’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: goldfire (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
What do you expect to happen here? We just don't have unboxed ints at
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:2 simonpj]: 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.2.2 => 8.2.3 Comment: It looks like this won't be fixed for 8.2.2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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# _) = '() | ^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: {{{#!hs {-# 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: {{{#!hs 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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?? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:7 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14180: Strange/bad error message binding unboxed type variable -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): To motivate why I want this, it's because the [http://hackage.haskell.org/package/kind-generics 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: {{{#!hs 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14180#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC