Opened 4 weeks ago
Last modified 4 weeks ago
#14155 new bug
GHC mentions unlifted types out of the blue (to me anyway)
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | highest | Milestone: | 8.4.1 |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | TypeInType | Cc: | RyanGlScott |
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
This one does me 'ead in, I accidentally type Ran
instead of Swap
{-# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #-} import Data.Coerce newtype Ran g h a = Ran (forall b. (a -> g b) -> h b) newtype Swap p f g a where Swap :: p g f a -> Swap p f g a deriving newtype Show class IxPointed m where ireturn :: a -> m i i a instance IxPointed f => IxPointed (Swap f) where ireturn :: forall a i. a -> Swap f i i a ireturn a = Ran (ireturn a)
and get this error
$ ghci -ignore-dot-ghci /tmp/bug.hs GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/bug.hs, interpreted ) /tmp/bug.hs:17:15: error: • Couldn't match expected type ‘Swap f i i a’ with actual type ‘Ran g0 h0 a0’ • In the expression: Ran (ireturn a) In an equation for ‘ireturn’: ireturn a = Ran (ireturn a) In the instance declaration for ‘IxPointed (Swap f)’ • Relevant bindings include a :: a (bound at /tmp/bug.hs:17:11) ireturn :: a -> Swap f i i a (bound at /tmp/bug.hs:17:3) | 17 | ireturn a = Ran (ireturn a) | ^^^^^^^^^^^^^^^ /tmp/bug.hs:17:20: error: • Couldn't match a lifted type with an unlifted type Expected type: (a0 -> g0 b) -> h0 b Actual type: (->) (a0 -> g0 b) (a0 -> g0 b) a • In the first argument of ‘Ran’, namely ‘(ireturn a)’ In the expression: Ran (ireturn a) In an equation for ‘ireturn’: ireturn a = Ran (ireturn a) | 17 | ireturn a = Ran (ireturn a) | ^^^^^^^^^ Failed, modules loaded: none.
Is GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of (->) :: TYPE rep -> TYPE rep' -> Type
Change History (6)
comment:2 Changed 4 weeks ago by
This feels similar
-- /tmp/bug.hs:6:12-20: error: -- • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’ -- When matching the kind of ‘'GHC.Types.LiftedRep’ -- • In the first argument of ‘R’, namely ‘(m `ibind`)’ -- In the expression: R (m `ibind`) -- In an equation for ‘lft’: lft m = R (m `ibind`) -- | -- 6 | lft m = R (m `ibind`) -- | ^^^^^^^^^ -- Failed, modules loaded: none. newtype R a = R ((a -> a) -> a) class IxMonad m where ibind :: (a -> m j k b) -> m i j a -> m i k b lft m = R (m `ibind`)
comment:3 Changed 4 weeks ago by
Keywords: | TypeInType added |
---|---|
Milestone: | → 8.4.1 |
Priority: | normal → highest |
Aha. Based on comment:1 I very rapidly found that the constraint solver was going wrong thus. We have
m :: k0 -> k0 -> * -> * i :: k0
and a wanted constraint
[W] (m i :: k0 -> * -> *) ~# ((->) LR LR :: * -> * -> *)
where LR
is LiftedRep
. This much is fine. But then the canonicaliser decomposes it thus
[W] (i :: k0) ~# (LR :: *) [W] (m :: k0 -> k0 -> * -> *) ~# ((->) LR :: forall r. * -> TYPE r -> *)
which is utterly bogus.
Presumably we need an extra guard in the can_eq_app
that checks that neither function kind is a forall?
Richard please comment.
comment:4 Changed 4 weeks ago by
Agreed with extra check -- but it should check for the fact that neither is a forall or both are foralls. I don't see a problem in decomposing a dependent application in this way.
Here's a simpler version which removes some cruft:
This is a regression from 8.0.2, where the error message didn't mention unlifted types: