Opened 3 months ago

Closed 3 months ago

Last modified 3 months ago

#13822 closed bug (fixed)

GHC not using injectivity?

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 8.0.1
Keywords: InjectiveFamilies, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T13822
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This may be normal behavior but.. (Example from System FC with Explicit Kind Equality)

{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}

import Data.Kind

data KIND = STAR | KIND :> KIND

data Ty :: KIND -> Type where
  TInt   :: Ty STAR
  TBool  :: Ty STAR
  TMaybe :: Ty (STAR :> STAR)
  TApp   :: Ty (a :> b) -> (Ty a -> Ty b)

type family
  IK (k :: KIND) = (res :: Type) | res -> k where
  IK STAR   = Type
  IK (a:>b) = IK a -> IK b

type family
  I (t :: Ty k) = (res :: IK k) | res -> t where
  I TInt       = Int
  I TBool      = Bool
  I TMaybe     = Maybe
  I (TApp f a) = (I f) (I a)

data TyRep (k :: KIND) (t :: Ty k) where
  TyInt   :: TyRep STAR         TInt
  TyBool  :: TyRep STAR         TBool
  TyMaybe :: TyRep (STAR:>STAR) TMaybe
  TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)

zero :: TyRep STAR a -> I a
zero = \case
  TyInt           -> 0
  TyBool          -> False
  TyApp TyMaybe _ -> Nothing

When I ask it to infer the representation for Int and Bool it does so with no surprises

-- Inferred type: 
-- 
-- int :: TyRep STAR TInt -> Int
int rep = zero rep :: Int


-- bool:: TyRep STAR TBool -> Bool
bool rep = zero rep :: Bool

but inferring the representation for Maybe Int fails

-- v.hs:43:16: error:
--     • Couldn't match kind ‘k’ with ‘'STAR’
--       ‘k’ is a rigid type variable bound by
--         the inferred type of
--         maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>
--                     TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
--         at v.hs:25:3
--       When matching the kind of ‘'TMaybe’
--       Expected type: Maybe Int
--         Actual type: I ('TApp 'TMaybe 'TInt)
--     • In the expression: zero rep :: Maybe Int
--       In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
--     • Relevant bindings include
--         rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)
--         maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
--           (bound at v.hs:43:1)
-- Failed, modules loaded: none.
maybeInt rep = zero rep :: Maybe Int

even though I is injective and GHC knows that I (TMaybe TApp TMaybe) = Maybe Int

>>> :kind! I (TMaybe `TApp` TInt)
I (TMaybe `TApp` TInt) :: IK 'STAR
= Maybe Int

Change History (6)

comment:1 Changed 3 months ago by Iceland_jack

Output I do not understand, with explicit kinds / coercions

/tmp/v.hs:41:16: error:
    • Couldn't match kind ‘k’ with ‘'STAR’
      ‘k’ is a rigid type variable bound by
        the inferred type of
        maybeInt :: ((I 'STAR
                        ('TInt |> Sym (Ty U(hole:{a2uB}, k1, 'STAR)_N)_N) :: IK * 'STAR)
                     ~~
                     ((Int |> Sym Main.D:R:IK[0]) :: IK * 'STAR),
                     (I ('STAR ':> 'STAR)
                        ('TMaybe |> Sym
                                      (Ty
                                         (U(hole:{a2uB}, k1, 'STAR)_N
                                          ':> U(hole:{a2uC}, k, 'STAR)_N)_N)_N) :: IK
                                                                                     *
                                                                                     ('STAR
                                                                                      ':> 'STAR))
                     ~~
                     ((Maybe |> Sym
                                  (Main.D:R:IK[1] <'STAR>_N <'STAR>_N
                                   ; Sym (Sym Main.D:R:IK[0] -> Sym Main.D:R:IK[0]))) :: IK
                                                                                           *
                                                                                           ('STAR
                                                                                            ':> 'STAR))) =>
                    TyRep
                      'STAR
                      ('TApp
                         'STAR
                         'STAR
                         ('TMaybe |> Sym
                                       (Ty
                                          (U(hole:{a2uB}, k1, 'STAR)_N
                                           ':> U(hole:{a2uC}, k, 'STAR)_N)_N)_N)
                         ('TInt |> Sym (Ty U(hole:{a2uB}, k1, 'STAR)_N)_N))
                    -> Maybe Int
        at /tmp/v.hs:23:3
      When matching types
        ('TMaybe |> Sym
                      (Ty
                         (U(hole:{a2uB}, k1, 'STAR)_N
                          ':> U(hole:{a2uC}, k, 'STAR)_N)_N)_N) :: Ty (k1 ':> k)
        'TMaybe :: Ty ('STAR ':> 'STAR)
      Expected type: Maybe Int
        Actual type: (I 'STAR
                        ('TApp
                           'STAR
                           'STAR
                           ('TMaybe |> Sym
                                         (Ty
                                            (U(hole:{a2uB}, k1, 'STAR)_N
                                             ':> U(hole:{a2uC}, k, 'STAR)_N)_N)_N)
                           ('TInt |> Sym
                                       (Ty U(hole:{a2uB}, k1, 'STAR)_N)_N)) |> Main.D:R:IK[0])
    • In the expression: zero rep :: Maybe Int
      In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
    • Relevant bindings include
        rep :: TyRep
                 'STAR
                 ('TApp
                    'STAR
                    'STAR
                    ('TMaybe |> Sym
                                  (Ty
                                     (U(hole:{a2uB}, k1, 'STAR)_N
                                      ':> U(hole:{a2uC}, k, 'STAR)_N)_N)_N)
                    ('TInt |> Sym (Ty U(hole:{a2uB}, k1, 'STAR)_N)_N))
          (bound at /tmp/v.hs:41:10)
        maybeInt :: TyRep
                      'STAR
                      ('TApp
                         'STAR
                         'STAR
                         ('TMaybe |> Sym
                                       (Ty
                                          (U(hole:{a2uB}, k1, 'STAR)_N
                                           ':> U(hole:{a2uC}, k, 'STAR)_N)_N)_N)
                         ('TInt |> Sym (Ty U(hole:{a2uB}, k1, 'STAR)_N)_N))
                    -> Maybe Int
          (bound at /tmp/v.hs:41:1)
Failed, modules loaded: none.

comment:2 Changed 3 months ago by Iceland_jack

Resolution: fixed
Status: newclosed

Never mind, this works in 8.3

comment:3 Changed 3 months ago by RyanGlScott

Yes, I suspect that this is a slightly more involved version of #11348.

comment:4 Changed 3 months ago by simonpj

Would someone like to add it as a regression test? It never does any harm!

comment:5 Changed 3 months ago by bgamari

Milestone: 8.2.1
Test Case: typecheck/should_compile/T13822

comment:6 Changed 3 months ago by Ben Gamari <ben@…>

In 04ca036/ghc:

testsuite: Add testcase for #13822

Reviewers: austin

Subscribers: rwbarton, thomie

GHC Trac Issues: #13822

Differential Revision: https://phabricator.haskell.org/D3655
Note: See TracTickets for help on using tickets.