Opened 3 months ago

Last modified 3 months 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:1 Changed 3 months ago by RyanGlScott

Cc: RyanGlScott added

Here's a simpler version which removes some cruft:

newtype R a = R ((a -> a) -> a)

newtype Swap p f g a = Swap (p g f a)

class IxPointed m where
  ireturn :: a -> m i i a

instance IxPointed f => IxPointed (Swap f) where
  ireturn a = R (ireturn a)
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:9:15: error:
    • Couldn't match expected type ‘Swap f i i a’
                  with actual type ‘R a’
    • In the expression: R (ireturn a)
      In an equation for ‘ireturn’: ireturn a = R (ireturn a)
      In the instance declaration for ‘IxPointed (Swap f)’
    • Relevant bindings include
        a :: a (bound at Bug.hs:9:11)
        ireturn :: a -> Swap f i i a (bound at Bug.hs:9:3)
  |
9 |   ireturn a = R (ireturn a)
  |               ^^^^^^^^^^^^^

Bug.hs:9:18: error:
    • Couldn't match a lifted type with an unlifted type
    • In the first argument of ‘R’, namely ‘(ireturn a)’
      In the expression: R (ireturn a)
      In an equation for ‘ireturn’: ireturn a = R (ireturn a)
    • Relevant bindings include
        a :: a (bound at Bug.hs:9:11)
        ireturn :: a -> Swap f i i a (bound at Bug.hs:9:3)
  |
9 |   ireturn a = R (ireturn a)
  |                  ^^^^^^^^^

This is a regression from 8.0.2, where the error message didn't mention unlifted types:

$ /opt/ghc/8.0.2/bin/ghci Bug.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:9:15: error:
    • Couldn't match expected type ‘Swap f i i a’
                  with actual type ‘R a’
    • In the expression: R (ireturn a)
      In an equation for ‘ireturn’: ireturn a = R (ireturn a)
      In the instance declaration for ‘IxPointed (Swap f)’
    • Relevant bindings include
        a :: a (bound at Bug.hs:9:11)
        ireturn :: a -> Swap f i i a (bound at Bug.hs:9:3)

Bug.hs:9:18: error:
    • Couldn't match type ‘m0 (a -> a)’ with ‘(->)’
      Expected type: (a -> a) -> a
        Actual type: m0 (a -> a) (a -> a) a
    • In the first argument of ‘R’, namely ‘(ireturn a)’
      In the expression: R (ireturn a)
      In an equation for ‘ireturn’: ireturn a = R (ireturn a)
    • Relevant bindings include
        a :: a (bound at Bug.hs:9:11)
        ireturn :: a -> Swap f i i a (bound at Bug.hs:9:3)
Last edited 3 months ago by RyanGlScott (previous) (diff)

comment:2 Changed 3 months ago by Iceland_jack

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 3 months ago by simonpj

Keywords: TypeInType added
Milestone: 8.4.1
Priority: normalhighest

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 3 months ago by goldfire

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.

comment:5 Changed 3 months ago by simonpj

OK: might you do this? Not hard, it seems.

comment:6 Changed 3 months ago by goldfire

Sure.

Note: See TracTickets for help on using tickets.