Core Lint error

[Iceland_jack]

{-# Language PartialTypeSignatures #-}
{-# Language TypeFamilyDependencies, KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language DataKinds #-}
{-# Language TypeFamilies #-}
{-# Language RankNTypes #-}
{-# Language NoImplicitPrelude #-}
{-# Language FlexibleContexts #-}
{-# Language MultiParamTypeClasses #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language FlexibleInstances #-}
{-# Language TypeOperators #-}
{-# Language ScopedTypeVariables #-}
{-# Language DefaultSignatures #-}
{-# Language FunctionalDependencies #-}
{-# Language UndecidableSuperClasses #-}
{-# Language UndecidableInstances #-}
{-# Language TypeInType #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language InstanceSigs, TypeApplications #-}

import Data.Monoid
import Data.Kind

data family Sing (a::k)

class SingKind k where
  type Demote k = (res :: Type) | res -> k
  fromSing :: Sing (a::k) -> Demote k

class SingI (a::k) where
  sing :: Sing a

data ACT  :: Type -> Type -> Type
data MHOM :: Type -> Type -> Type

type m ·-  a  = ACT  m a  -> Type
type m ·-> m' = MHOM m m' -> Type

class Monoid m => Action (act :: m ·- a) where
  act :: m -> (a -> a)

class (Monoid m, Monoid m') => MonHom (mhom :: m ·-> m') where
  monHom :: m -> m'

data MonHom_Distributive m :: (m ·- a) -> (a ·-> a)

type Good k = (Demote k ~ k, SingKind k)

instance (Action act, Monoid a, Good m) => MonHom (MonHom_Distributive m act :: a ·-> a) where
  monHom :: a -> a
  monHom = act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) where

fails on 8.2.1 and 8.3.20171208 when passed -fdefer-type-errors -dcore-lint, full log attached

$ ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint 146-bug.hs 
GHCi, version 8.3.20171208: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 146-bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: warning:
    In the expression: fromSing
                         @ m_a2Ju
...

[simonpj]

Yurgh. I don't yet understand the details, but what is happening is something like this. We have an implication constraint

forall x[2].
   [W] co1: alpaha[1] ~ ty |> co2
   [W] co2: k1 ~ *

Here co2 is an ultimately-unsolved kind coercion. We float co1 out of the implication and unify with alpha. Then in TcErrors we make evidence for co2 using a call to error, bound in the EvBinds for the implication.

But alas the scope of the binding for co2 is just the term enclosed by the implication constraint. But the use of co2 has escaped, in the type alpha.

Yikes. This only shows up with deferred type errors, because normally we don't make term-level bindings for coercions; instead we just side-effect them right into the coercions they are used in, which just happens to work even in the "escaping" case. But with deferred type errors we need to force a term-level error, and to do so in as narrow a scope as possible.

I'd like a smaller test case to show this up.

I really do not know how to solve this. It's all because of those pesky casts inside types! Richard, your advice would be valuable here.

[monoidal]

I've reduced to:

{-# Language PartialTypeSignatures #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language TypeApplications #-}

f :: forall m. ()
f = id @m :: _

and as previously ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint 146-bug.hs gives a Core Lint error; I've checked 8.2.1 but not HEAD.

[goldfire]

Why doesn't co2 float out? We really shouldn't float co1 out if we don't float co2 out. The fact that it works without deferred type errors is just a fluke, really. (What if co2 ends up being filled in with a coercion that mentions x?)

I think this can be fixed just by adding a little more logic to the float-out code. Unfortunately, it also means that we need to calculate floating-out in dependency order (so we can process co2 before even looking at co1. It makes the floating-out code a little more intricate, but the complication should be quite local.

Does that sound reasonable?

[simonpj]

What if co2 ends up being filled in with a coercion that mentions x?

Excellent question! But even a more complicated floating isn't enough. Suppose co2 is actually solved. Then its binding will live in the inner implication; so we then can't float co1. And if that solved binding did mention x, then we should presumably not float co1. Yikes. This works today because: if co2 is solved, when we zonk co1 we'll see all the free vars of co1 (because of the update in place stuff).

In truth, if coercions generated bindings in the implication, we'd have to float them too, assuming none of them mention the skolemised variables.

Bottom line: it seems delicate, but yes perhaps doing transitive capture would nail it.

[simonpj]

...or not. Monoidal's example is amazing. Here's the constraint we get (before simplifying it):

simplifyTop {
  wanted =  WC {wc_impl =
                  Implic {
                    TcLevel = 2
                    Skolems = k_aGF[sk:2] (m_aGG[sk:2] :: k_aGF[sk:2])
                    No-eqs = False
                    Status = Unsolved
                    Given =
                    Wanted =
                      WC {wc_simple =
                            [WD] hole{aGP} {0}:: ((m_aGG[sk:2] |> {aGN})
                                                  -> (m_aGG[sk:2] |> {aGN}) :: *)
                                                 GHC.Prim.~# (() :: *) (CNonCanonical)
                          wc_impl =
                            Implic {
                              TcLevel = 3
                              Skolems =
                              No-eqs = False
                              Status = Unsolved
                              Given =
                              Wanted =
                                WC {wc_simple =
                                      [D] _ {0}:: (m_aGG[sk:2] |> {aGN})
                                                  -> (m_aGG[sk:2] |> {aGN}) (CHoleCan: TypeHole(_))
                                      [WD] hole{aGN} {0}:: (k_aGF[sk:2] :: *)
                                                           GHC.Prim.~# (* :: *) (CNonCanonical)}
                              Binds = EvBindsVar<aGO>
                              Needed = []
                              the inferred type of <expression>_02y :: w_aGJ[tau:3] }}
                    Binds = EvBindsVar<aGQ>
                    Needed = []
                    the type signature for:
                      f :: forall k (m :: k). () }}

Notice that the coercion {aGN} is a Wanted inside the inner implication constraint, but is used in a constraint (for {aGP}) outside that implication. No amount of floating is going to put that right!

[simonpj]

We don't even need a partial type signature. This gives a similar Lint error (when compiled with -fdefer-type-errrors:

g :: forall m. ()
g = let h = id @m
    in h

[goldfire]

comment:6 is frightening. I can look into this in due course, but do you see how on earth that happens? I wonder if that's a separate bug.

[Simon Peyton Jones <simonpj@…>]

In a492af06/ghc:

Refactor coercion holes

In fixing Trac #14584 I found that it would be /much/ more
convenient if a "hole" in a coercion (much like a unification
variable in a type) acutally had a CoVar associated with it
rather than just a Unique.  Then I can ask what the free variables
of a coercion is, and get a set of CoVars including those
as-yet-un-filled in holes.

Once that is done, it makes no sense to stuff coercion holes
inside UnivCo.  They were there before so we could know the
kind and role of a "hole" coercion, but once there is a CoVar
we can get that info from the CoVar.  So I removed HoleProv
from UnivCoProvenance and added HoleCo to Coercion.

In summary:

* Add HoleCo to Coercion and remove HoleProv from UnivCoProvanance

* Similarly in IfaceCoercion

* Make CoercionHole have a CoVar in it, not a Unique

* Make tyCoVarsOfCo return the free coercion-hole variables
  as well as the ordinary free CoVars.  Similarly, remember
  to zonk the CoVar in a CoercionHole

We could go further, and remove CoercionHole as a distinct type
altogther, just collapsing it into HoleCo.  But I have not done
that yet.

[Simon Peyton Jones <simonpj@…>]

In f5cf9d1a/ghc:

Fix floating of equalities

This rather subtle patch fixes Trac #14584.  The problem was
that we'd allowed a coercion, bound in a nested scope, to escape
into an outer scope.

The main changes are

* TcSimplify.floatEqualities takes more care when floating
  equalities to make sure we don't float one out that mentions
  a locally-bound coercion.
  See Note [What prevents a constraint from floating]

* TcSimplify.emitResidualConstraints (which emits the residual
  constraints in simplifyInfer) now avoids burying the constraints
  for escaping CoVars inside the implication constraint.

* Since I had do to this stuff with CoVars, I moved the
  fancy footwork about not quantifying over CoVars from
  TcMType.quantifyTyVars to its caller
  TcSimplify.decideQuantifiedTyVars.  I think its other
  callers don't need to worry about all this CoVar stuff.

This turned out to be surprisigly tricky, and took me a solid
day to get right.  I think the result is reasonably neat, though,
and well documented with Notes.

[simonpj]

Blimey. That rabbit-hole was a lot deeper than I expected.