Opened 3 years ago

Closed 3 years ago

#13197 closed bug (invalid)

Perplexing levity polymorphism issue

Reported by: bgamari Owned by:
Priority: highest Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.1
Keywords: typeable Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

I would have expected this to compile since the levity polymorphism patch (along with Phab:D2038) was merged, but sadly it seems the typechecker isn't quite clever enough yet (or perhaps I'm the not clever one),

{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
             TypeOperators, ViewPatterns #-}
{-# LANGUAGE TypeInType #-}

module Test where

import Data.Kind
import GHC.Exts

data TypeRep (a :: k) where
  TypeCon :: String -> TypeRep a
  TypeApp :: forall k1 k2 (f :: k1 -> k2) (x :: k1). TypeRep f -> TypeRep x -> TypeRep (f x)
  TypeFun :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). TypeRep a -> TypeRep b -> TypeRep (a -> b)

data SomeTypeRep where
  SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep

data (a :: k1) :~~: (b :: k2) where
   HRefl :: a :~~: a

eqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)
eqTypeRep = undefined

typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined

toApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep
toApp (SomeTypeRep f) (SomeTypeRep a)
  | TypeFun arg res <- typeRepKind f
  , Just HRefl <- arg `eqTypeRep` typeRepKind a
  = Just $ SomeTypeRep (TypeApp f a)
toApp _ _ = Nothing

Change History (4)

comment:1 Changed 3 years ago by bgamari

Description: modified (diff)

comment:2 Changed 3 years ago by bgamari

For the record the above fails with,

Test.hs:34:33: error:
    • Could not deduce: (r2 :: RuntimeRep)
                        ~~
                        ('LiftedRep :: RuntimeRep)
      from the context: ((* :: *) ~~ (* :: *),
                         (k :: *) ~~ ((a2 -> b) :: *))
        bound by a pattern with constructor:
                   TypeFun :: forall (a :: TYPE r1) (b :: TYPE r2).
                              TypeRep (TYPE r1) a -> TypeRep (TYPE r2) b -> TypeRep * (a -> b),
                 in a pattern binding in
                      pattern guard for
                      an equation for ‘toApp’
        at Test.hs:32:5-19
      or from: ((* :: *) ~~ (TYPE r1 :: *), (k1 :: *) ~~ (a2 :: TYPE r1))
        bound by a pattern with constructor:
                   HRefl :: forall k2 (a :: k2). (:~~:) k2 k2 a a,
                 in a pattern binding in
                      pattern guard for
                      an equation for ‘toApp’
        at Test.hs:33:10-14
      ‘r2’ is a rigid type variable bound by
        a pattern with constructor:
          TypeFun :: forall (a :: TYPE r1) (b :: TYPE r2).
                     TypeRep (TYPE r1) a -> TypeRep (TYPE r2) b -> TypeRep * (a -> b),
        in a pattern binding in
             pattern guard for
             an equation for ‘toApp’
        at Test.hs:32:5-19
      When matching the kind of ‘b’
      Expected type: TypeRep (k1 -> b) a
        Actual type: TypeRep k a
    • In the first argument of ‘TypeApp’, namely ‘f’
      In the first argument of ‘SomeTypeRep’, namely ‘(TypeApp f a)’
      In the second argument of ‘($)’, namely ‘SomeTypeRep (TypeApp f a)’
    • Relevant bindings include
        res :: TypeRep (TYPE r2) b (bound at Test.hs:32:17)
   |
34 |   = Just $ SomeTypeRep (TypeApp f a)
   |                                 ^

comment:3 Changed 3 years ago by goldfire

This is expected behavior. Well, for me. After I've studied it and revised my expectation.

The problem is that k2 in the type of TypeApp has kind Type. But f a's kind, res, has type TYPE r2, which we see looking at the type of TypeFun. So we get a type error.

The fix is to convince GHC that f a's type's kind is really Type. And we can do that with one extra check:

toApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep
toApp (SomeTypeRep f) (SomeTypeRep a)
  | TypeFun arg res <- typeRepKind f
  , Just HRefl <- arg `eqTypeRep` typeRepKind a
  , Just HRefl <- typeRepKind res `eqTypeRep` (undefined :: TypeRep Type)
  = Just $ SomeTypeRep (TypeApp f a)
toApp _ _ = Nothing

This compiles for me. Note that arg's kind is discovered to be Type because arg equals the result of a typeRepKind, which always has kind Type.

Fun times!

GHC should really come little trophies that you can accrue by triggering certain bizarre scenarios.

comment:4 Changed 3 years ago by goldfire

Resolution: invalid
Status: newclosed
Note: See TracTickets for help on using tickets.