Opened 19 months ago

Closed 19 months ago

Last modified 19 months ago

#11642 closed bug (invalid)

Heterogeneous type equality evidence ignored

Reported by: bgamari Owned by: goldfire
Priority: highest Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.3
Keywords: TypeInType Cc: simonpj
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

Either that or I am missing something...

Consider the following,

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

module Test where

data TypeRep (a :: k) where
  TypeCon :: String -> TypeRep a
  TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)

data TypeRepX where
  TypeRepX :: TypeRep a -> TypeRepX

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

trArrow :: TypeRep (->)
trArrow = undefined

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

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

pattern TRFun :: forall fun. ()
              => forall arg res. (fun ~ (arg -> res))
              => TypeRep arg
              -> TypeRep res
              -> TypeRep fun
pattern TRFun arg res <- TypeApp (TypeApp (eqTypeRep trArrow -> Just HRefl) arg) res

buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
  case typeRepKind f of
    TRFun arg _ ->
      case eqTypeRep arg x of
        Just HRefl ->
          TypeRepX $ TypeApp f x

This fails with,

$ ghc Test.hs -fprint-explicit-kinds
[1 of 1] Compiling Test             ( Test.hs, Test.o )

Test.hs:38:30: error:
    • Expected kind ‘TypeRep (k1 -> res) a’,
        but ‘f’ has kind ‘TypeRep k a’
    • In the first argument of ‘TypeApp’, namely ‘f’
      In the second argument of ‘($)’, namely ‘TypeApp f x’
      In the expression: TypeRepX $ TypeApp f x
    • Relevant bindings include
        arg :: TypeRep * arg (bound at Test.hs:35:11)

That is, the typechecker doesn't believe that f's type (why is it saying "kind" here?), TypeRep k a, will unify with TypeRep (k1 -> res) a, despite the TRFun pattern match, which should have brought into scope that k ~ (arg -> res).

This was tested with a recent snapshot from ghc-8.0 (23baff798aca5856650508ad0f7727045efe3680).

Am I missing something here or is this a bug?

Change History (11)

comment:1 Changed 19 months ago by goldfire

Looks like a bug to me.

Also you're right that the error message should say "type".

comment:2 Changed 19 months ago by bgamari

The problem isn't actually the pattern synonym at all. Even the straightforward nested-case approach fails in the same way,

buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
  case typeRepKind f of
    TypeApp (TypeApp ty arg) res ->
      case eqTypeRep trArrow ty of
        Just HRefl ->
          case eqTypeRep arg x of
            Just HRefl ->
              TypeRepX $ TypeApp f x

comment:3 Changed 19 months ago by bgamari

Cc: simonpj added

Make sure Simon sees this.

comment:4 Changed 19 months ago by bgamari

Summary: Typechecker doesn't use evidence available from pattern synonym?Heterogeneous type equality evidence ignored

comment:5 Changed 19 months ago by bgamari

Judging by the -ddump-tc-trace output (for the fully expanded case version given in comment:2), the problem is that this wanted is unsolved,

wanted :: (~#) k1 k1
               x1 ((TYPE |> <Levity>_N -> Sym cobox_a1Mi) 'Lifted) (CNonCanonical)}

given these givens,

(~#) * *
     k2 (f1 x2)

(~#) (k3 -> *) (k3 -> *)
     f1 (f2 x1)

(~#) * *
     (* -> * -> *) (k1 -> k3 -> *)

(~#) (* -> * -> *) (k1 -> k3 -> *)
     (->) f2

(~#) * *
     k1 k4

(~#) k1 k4
     x1 a
Last edited 19 months ago by bgamari (previous) (diff)

comment:6 Changed 19 months ago by bgamari

Oddly enough, if I ask for the same wanted in a slightly more direct way, things work,

data IsFunc' a b where
  IsFunc' :: forall x y a b (f :: x -> y).
             IsFunc' (TypeRep f) (TypeRep x)

buildApp :: forall k. forall (a :: k) b.
            TypeRep a -> TypeRep b -> IsFunc' (TypeRep a) (TypeRep b)
buildApp f x =
  case typeRepKind f of
    TypeApp (TypeApp ty arg) res ->
      case eqTypeRep trArrow ty of
        Just HRefl ->
          case eqTypeRep arg x of
            Just HRefl ->
              IsFunc'

comment:7 Changed 19 months ago by bgamari

Priority: highhighest

Bumping in priority.

Last edited 19 months ago by bgamari (previous) (diff)

comment:8 Changed 19 months ago by simonpj

Keywords: TypeInType added

Richard I think this needs your loving care. I had a look but ran out of time in a maze of twisty little casts, all alike.

comment:9 Changed 19 months ago by bgamari

Owner: set to goldfire

comment:10 Changed 19 months ago by goldfire

Resolution: invalid
Status: newclosed

A maze this is, indeed. But, happily(?), we humans were the ones lost, not GHC, which is spot on.

The original code is

buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
  case typeRepKind f of
    TRFun arg _ ->
      case eqTypeRep arg x of
        Just HRefl ->
          TypeRepX $ TypeApp f x

Let me augment with some kinds and such:

buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
  -- f :: TypeRep kind_tf (tf :: kind_tf)
  -- x :: TypeRep kind_tx (tx :: kind_tx)
  case typeRepKind f of
    TRFun arg _ ->
      -- arg :: TypeRep kind_targ (targ :: kind_targ)
      -- _   :: TypeRep kind_tres (tres :: kind_tres)
      -- _   :: kind_tf ~ (targ -> tres)
      -- _   :: kind_targ ~ *
      -- _   :: kind_tres ~ *
      case eqTypeRep arg x of
        Just HRefl ->
          -- _ :: kind_targ ~ kind_tx   (but kind_targ ~ *)
          -- _ :: targ      ~ tx
          TypeRepX $ TypeApp f x
            -- NEED: exists k1 k2.
            --   kind_tf ~ k1 -> k2
            --   kind_tx ~ k1

At the end, we need to find k1 and k2 such that those two equalities are provable from our givens. The choice of k1 and k2 is quite clear: choose k1 := targ and k2 := tres. Now, we must prove kind_tx ~ targ. But we can't! We know that targ ~ tx, not targ ~ kind_tx. Note that, actually, kind_tx is really known to be *. So GHC helpfully reports

T11642.hs:47:30: error:
    • Could not deduce: arg ~ *
      from the context: k ~ (arg -> res)
        bound by a pattern with pattern synonym:
                   TRFun :: forall fun arg res.
                            (fun ~ (arg -> res)) =>
                            TypeRep arg -> TypeRep res -> TypeRep fun,
                 in a case alternative
        at T11642.hs:37:5-15
      or from: (* ~ k1, arg ~ a1)
        bound by a pattern with constructor:
                   HRefl :: forall k2 (a :: k2). a :~~: a,
                 in a case alternative
        at T11642.hs:44:14-18
      ‘arg’ is a rigid type variable bound by
        a pattern with pattern synonym:
          TRFun :: forall fun arg res.
                   (fun ~ (arg -> res)) =>
                   TypeRep arg -> TypeRep res -> TypeRep fun,
        in a case alternative
        at T11642.hs:37:5
      Expected type: TypeRep a
        Actual type: TypeRep a
    • In the first argument of ‘TypeApp’, namely ‘f’
      In the second argument of ‘($)’, namely ‘TypeApp f x’
      In the expression: TypeRepX $ TypeApp f x
    • Relevant bindings include
        arg :: TypeRep arg (bound at T11642.hs:37:11)

Which is absolutely correct.

Happily, fixing the code is easy:

-- ...
      case eqTypeRep arg (typeRepKind x) of
-- ...

works like a charm.

I do believe some intermediate work (between when this was reported and now) has improved this message. It's still not great, given that it took me the better part of an hour to deduce all of the above. But I don't see how we can do better without giving the user the trail of breadcrumbs that GHC used to find its result. (I do think we should give this ability to the user, somehow. It would be easy enough to implement -- just augment CtLoc to keep track of previous constraints and how they were transformed. The data is all there.)

I'm thus closing this as invalid. I'm also not adding a regression test, because I'm not thrilled with the error message as it is, and there's no other unusual behavior here.

comment:11 Changed 19 months ago by bgamari

Oh dear, what a silly mistake on my part. Thanks for tracking this down Richard.

Note: See TracTickets for help on using tickets.