RE: Panic from rewritableTyVarsOfType

[Simon Peyton Jones via ghc-devs]

|  Typeable1.hs:22:5: error:
|  • Couldn't match kind ‘* -> (* -> *) -> (* -> *) -> * -> *’
|  with ‘forall k. (* -> *) -> (k -> *) -> k -> *’

I still don't see why we end up equating a polykind with a kind.

|  Anyways, hopefully this will be resolved with the fix to Simon's second
|  issue. Otherwise I just need to look at two performance regressions and I
|  think I'm done.

I'm validating a patch that uses tyCoVarsOfType, but a bit more selectively. So 
you'll get the same error.

S   

|  -Original Message-
|  From: Ben Gamari [mailto:b...@smart-cactus.org]
|  Sent: 03 February 2017 16:01
|  To: Simon Peyton Jones <simo...@microsoft.com>; Richard Eisenberg
|  <r...@cs.brynmawr.edu>
|  Cc: ghc-devs@haskell.org
|  Subject: RE: Panic from rewritableTyVarsOfType
|  
|  Ben Gamari <b...@smart-cactus.org> writes:
|  
|  > Simon Peyton Jones <simo...@microsoft.com> writes:
|  >
|  >> Meanwhile to get you rolling, you can replace rewritableTyVars with
|  >> tyCoVarsOfType and it'll all work, just a bit less efficiently.
|  >>
|  > Thanks Simon! Indeed that allows things to proceed and in the process,
|  > confirms that there is a bug in my solver logic.
|  >
|  I should clarify: the bug is in fact not in the Typeable solver. The problem
|  is that we have a type with some kind polymorphism. For instance,
|  
|  data Proxy (a :: k) = Proxy
|  
|  Note that in order to be `Typeable` Proxy needs to have its `k` kind
|  argument instantiated. Consequently this program is perfectly fine,
|  
|  ty :: TypeRep (Proxy Int)
|  ty = typeRep
|  
|  We can even decompose this into a type application,
|  
|  case ty of
|TRApp a b  -> ...
|  
|  where `a :: TypeRep Proxy` (with `k ~ Type`) and `b :: TypeRep Int`.
|  However, if we attempt to decompose `a` again (which is what the
|  Typeable1 testcase described in this thread tests), we run into trouble,
|  
|  case a of
|TRApp x y -> ...
|  
|  After changing rewritableTyVars with tyCoVarsOfType, the testcase
|  Typeable1 fails with the following correct, albeit not terribly readable,
|  error message,
|  
|  Typeable1.hs:22:5: error:
|  • Couldn't match kind ‘* -> (* -> *) -> (* -> *) -> * -> *’
|  with ‘forall k. (* -> *) -> (k -> *) -> k -> *’
|Inaccessible code in
|  a pattern with pattern synonym:
|TRApp :: forall k2 (t :: k2).
|() =>
|forall k1 (a :: k1 -> k2) (b :: k1).
|t ~ a b =>
|TypeRep (k1 -> k2) a -> TypeRep k1 b -> TypeRep k2 t,
|  in a pattern binding in
|  'do' block
|  • In the pattern: TRApp x y
|In a stmt of a 'do' block: TRApp x y <- pure x
|In the expression:
|  do let x :: ComposeK Maybe Maybe Int
|x = undefined
|TRApp x y <- pure $ typeOf x
|print (x, y)
|TRApp x y <- pure x
|
|  • Relevant bindings include
|  y :: TypeRep k3 b2 (bound at Typeable1.hs:19:13)
|  x :: TypeRep (k3 -> k2 -> k1 -> *) a2 (bound at
|  Typeable1.hs:19:11)
|  
|  This might be a place where GHC could hold the user's hand a bit more
|  gently.
|  
|  Anyways, hopefully this will be resolved with the fix to Simon's second
|  issue. Otherwise I just need to look at two performance regressions and I
|  think I'm done.
|  
|  Cheers,
|  
|  - Ben
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Panic from rewritableTyVarsOfType

[Ben Gamari]

Ben Gamari  writes:

> Simon Peyton Jones  writes:
>
>> Meanwhile to get you rolling, you can replace rewritableTyVars with
>> tyCoVarsOfType and it'll all work, just a bit less efficiently.
>>
> Thanks Simon! Indeed that allows things to proceed and in the process,
> confirms that there is a bug in my solver logic.
>
I should clarify: the bug is in fact not in the Typeable solver. The
problem is that we have a type with some kind polymorphism. For
instance,

data Proxy (a :: k) = Proxy

Note that in order to be `Typeable` Proxy needs to have its `k` kind
argument instantiated. Consequently this program is perfectly fine,

ty :: TypeRep (Proxy Int)
ty = typeRep

We can even decompose this into a type application,

case ty of
  TRApp a b  -> ...

where `a :: TypeRep Proxy` (with `k ~ Type`) and `b :: TypeRep Int`.
However, if we attempt to decompose `a` again (which is what the
Typeable1 testcase described in this thread tests), we run into trouble,

case a of
  TRApp x y -> ...

After changing rewritableTyVars with tyCoVarsOfType, the testcase
Typeable1 fails with the following correct, albeit not terribly
readable, error message,

Typeable1.hs:22:5: error:
• Couldn't match kind ‘* -> (* -> *) -> (* -> *) -> * -> *’
with ‘forall k. (* -> *) -> (k -> *) -> k -> *’
  Inaccessible code in
a pattern with pattern synonym:
  TRApp :: forall k2 (t :: k2).
  () =>
  forall k1 (a :: k1 -> k2) (b :: k1).
  t ~ a b =>
  TypeRep (k1 -> k2) a -> TypeRep k1 b -> TypeRep k2 t,
in a pattern binding in
'do' block
• In the pattern: TRApp x y
  In a stmt of a 'do' block: TRApp x y <- pure x
  In the expression:
do let x :: ComposeK Maybe Maybe Int
  x = undefined
  TRApp x y <- pure $ typeOf x
  print (x, y)
  TRApp x y <- pure x
  
• Relevant bindings include
y :: TypeRep k3 b2 (bound at Typeable1.hs:19:13)
x :: TypeRep (k3 -> k2 -> k1 -> *) a2 (bound at Typeable1.hs:19:11)

This might be a place where GHC could hold the user's hand a bit more gently.

Anyways, hopefully this will be resolved with the fix to Simon's second
issue. Otherwise I just need to look at two performance regressions and
I think I'm done.

Cheers,

- Ben


signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Panic from rewritableTyVarsOfType

[Ben Gamari]

Simon Peyton Jones  writes:

> Ben, Richard
>
> rewritableTyVarsOfType is used when deciding whether to split a [WD]
> constraint into [W] and [D]. For example, if we are adding
>[WD] C a
> and there is an inert
>[WD] a ~ Int
> then we want to split the [WD] into
>[W] C a
>[D] C a
> so that the [D] one can be rewritten and perhaps yield improvement etc.
>
> There is no point in rewriting coercions or cases in t, because they
> won't help (C t) to reduce. That's why rewriteableTyVarsOfType differs
> from tyVarsOfType. And indeed the arg of a class C should be a
> monotype.
>
Ahh, I see.

> So rewriteableTyVarsOfType doesn't expect foralls, hence the panic.
> But it's seeing a forall in an /equality/ constraint.
>
> FIRST ISSUE: I'm a bit surprised about that (smacks of impredicative
> polymorphism) so the first thing to check is that this is really
> supposed to happen in this program. Richard should be able to help.
>
Indeed this test is meant to fail, just not with a panic. I suspect this
means that my solver logic isn't catching requests for polytypes as
early as it needs to.

> SECOND ISSUE: But regardless, I now realise that shouldSplitWD only
> needs to split a [WD] equality if the LHS matches. If we have
>[WD] a ~ ty   -- work item
>[D] a ~ ty2   -- inert
> then we want to split the [WD] so we can get [D] ty ~ ty2. But
> otherwise there is no point.
>
> Richard do you agree?
>
> I'll try that out.
>
> Meanwhile to get you rolling, you can replace rewritableTyVars with
> tyCoVarsOfType and it'll all work, just a bit less efficiently.
>
Thanks Simon! Indeed that allows things to proceed and in the process,
confirms that there is a bug in my solver logic.

Cheers,

- Ben



signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs