Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#12466 closed bug (fixed)

Typechecker regression: Inaccessible code in a type expected by the context

Reported by: RyanGlScott Owned by:
Priority: highest Milestone: 8.0.2
Component: Compiler (Type checker) Version: 8.1
Keywords: Cc: heisenbug, simonpj, ekmett
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T12466, T12466a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

The following compiles with GHC 8.0.1 and earlier, but not with GHC HEAD:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class Foo a where
  foo :: (a ~ Int => Int) -> a -> a
  foo _ a2 = a2

instance Foo Char
$ /opt/ghc/head/bin/ghc Bug.hs 
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:9:10: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Inaccessible code in
        a type expected by the context:
          Char ~ Int => Int
    • In the expression: Bug.$dmfoo @Char
      In an equation for ‘foo’: foo = Bug.$dmfoo @Char
      In the instance declaration for ‘Foo Char’

This causes lens-4.14 to fail to build with GHC HEAD.

The reason HEAD fails to compile lens, but GHC 8.0.1 works, is because the fix for #12220 is in HEAD, but not in 8.0.1.

Change History (40)

comment:1 Changed 3 years ago by RyanGlScott

Description: modified (diff)

comment:2 Changed 3 years ago by goldfire

According to current practice of making inaccessible code an error, I think the new behavior is more correct than the old one.

I think the fix for this is #11066.

comment:3 Changed 3 years ago by heisenbug

Cc: heisenbug added

comment:4 Changed 3 years ago by RyanGlScott

goldfire, are you saying this code should emit a warning? If so, what can be done to fix the code?

FWIW, this bug also prevents the constraints library from building with GHC HEAD, although the bug appears in a slightly different form. Here's a stripped-down example that compiles with GHC 8.0.1, but not GHC HEAD:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module ConstraintsBug where

import GHC.TypeLits (Nat)
import Unsafe.Coerce (unsafeCoerce)

data Dict a where
  Dict :: a => Dict a

newtype a :- b = Sub (a => Dict b)

axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))

type Divides n m = n ~ Gcd n m
type family Gcd :: Nat -> Nat -> Nat where

dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
dividesGcd = Sub axiom
$ /opt/ghc/head/bin/ghc ConstraintsBug.hs
[1 of 1] Compiling ConstraintsBug   ( ConstraintsBug.hs, ConstraintsBug.o )

ConstraintsBug.hs:26:14: error:
    • Couldn't match type ‘a’ with ‘Gcd a b’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          dividesGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat).
                        (Divides a b, Divides a c) :- Divides a (Gcd b c)
        at ConstraintsBug.hs:25:1-77
      Inaccessible code in
        a type expected by the context:
          (Divides a b, Divides a c) => Dict a ~ Gcd a (Gcd b c)
    • In the first argument of ‘Sub’, namely ‘axiom’
      In the expression: Sub axiom
      In an equation for ‘dividesGcd’: dividesGcd = Sub axiom
    • Relevant bindings include
        dividesGcd :: (Divides a b, Divides a c) :- Divides a (Gcd b c)
          (bound at ConstraintsBug.hs:26:1)

comment:5 Changed 3 years ago by mpickering

I don't think it is clear from this ticket how this code was expected to work in the past.

In previous versions, it was possible to use type signatures like this in order to state that only Int could provide a different definition from the default definition. So in Ryan's example, instance Foo Char would compile with the default definition for foo. This always seemed like a bug too me.

comment:6 Changed 3 years ago by RyanGlScott

To clarify, I think the constraints code is an occurrence of the same bug since

  1. dividesGcd's type signature has a context (Divides a b, which is the same as a ~ Gcd a b) in which GHC determines an equality is unattainable.
  2. The body of dividesGcd doesn't use the context, since it's defined in terms of axiom (a.k.a. unsafeCoerce).

comment:7 Changed 3 years ago by RyanGlScott

Cc: simonpj added

comment:8 Changed 3 years ago by goldfire

I think comment:4 is unrelated. (But let's not lose the fact that there is a terrible pretty-printing bug there, without parentheses around the equality argument to Dict.) The commit in comment:7 is all about instances, and comment:4 is unrelated to instances.

Yes, I think the original code should produce a warning. To suppress the warning, the user should include an implementation of foo, so that the generic-default implementation (which has the wrong type) is not used. But if inaccessible code is an error, then the original code should produce an error, just as it is now.

comment:9 Changed 3 years ago by RyanGlScott

Huh, I didn't think that manually implementing foo would fix the issue, but sure enough, this compiles without warnings on GHC HEAD:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class Foo a where
  foo :: (a ~ Int => Int) -> a -> a
  foo _ a2 = a2

instance Foo Char where
  foo _ a2 = a2

What I don't understand is how this code is any different from the default implementation. If the default implementation succeeds or fails, shouldn't copy-and-pasting it behave likewise?

Even stranger, adding the type signature manually via InstanceSigs causes it to fail to typecheck again:

{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class Foo a where
  foo :: (a ~ Int => Int) -> a -> a
  foo _ a2 = a2

instance Foo Char where
  foo :: (Char ~ Int => Int) -> Char -> Char
  foo _ a2 = a2
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:10: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Inaccessible code in
        the type signature for:
          foo :: Char ~ Int => Int
    • In the ambiguity check for ‘foo’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: foo :: (Char ~ Int => Int) -> Char -> Char
      In the instance declaration for ‘Foo Char’

Bug.hs:11:10: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Inaccessible code in
        the type signature for:
          foo :: Char ~ Int => Int
    • When checking that instance signature for ‘foo’
        is more general than its signature in the class
        Instance sig: (Char ~ Int => Int) -> Char -> Char
           Class sig: (Char ~ Int => Int) -> Char -> Char
      In the instance declaration for ‘Foo Char’

So I'm quite lost as to what's happening, and moreover, what should happen.

comment:10 Changed 3 years ago by goldfire

As described in the manual, a generic-default type signature (that is, one using the default keyword in a class definition) is more specific than the "normal" type signature for a class method. When no implementation is given for a method in an instance declaration, the default implementation is typechecked against the generic-default type signature.

In the code in the Description, this typecheck fails.

On the other hand, if we provide an implementation for foo, the generic-default signature is not consulted in the instance declaration, and so there is no problem.

When you add an InstanceSigs signature, then you're just writing a fresh signature that fails to typecheck. Your new signature is utterly unrelated to the generic-default signature.

Does this help to clarify?

comment:11 Changed 3 years ago by RyanGlScott

This example isn't using DefaultSignatures at all. That is, it's using a default method (which is Haskell 98), but not a generic default method (which requires a language extension). Moreover, the (non-generic) default method I gave is exactly the same as the manual implementation, yet one typechecks and the other doesn't.

comment:12 Changed 3 years ago by RyanGlScott

OK, I think I've got a hunch why this code is failing all of a sudden starting with GHC HEAD. As I mentioned earlier, this code was typechecking just fine up until d2958bd08a049b61941f078e51809c7e63bc3354. You can see what code ghc is filling in with -ddump-deriv:

$ /opt/ghc/head/bin/ghc Bug.hs -ddump-deriv
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

==================== Filling in method body ====================
Bug.Foo [GHC.Types.Char]
  Bug.foo = Bug.$dmfoo @GHC.Types.Char

If I try to implement something like $dmfoo manually, I can get the same error:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class Foo a where
  foo :: (a ~ Int => Int) -> a -> a
  foo = fooDefault

fooDefault :: (a ~ Int => Int) -> a -> a
fooDefault _ a2 = a2

instance Foo Char where
  foo = fooDefault @Char
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:14:9: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Inaccessible code in
        a type expected by the context:
          Char ~ Int => Int
    • In the expression: fooDefault @Char
      In an equation for ‘foo’: foo = fooDefault @Char
      In the instance declaration for ‘Foo Char’

So it's apparent that this behavior is different from before. Unfortunately, -ddump-deriv doesn't output this defaulting information on GHC 8.0.1 and earlier, so all we have to work with is -ddump-simpl. Compiling the original program with -ddump-simpl on GHC 8.0.1 yields:

-- RHS size: {terms: 3, types: 7, coercions: 0}
$cfoo_rCm :: ((Char :: *) ~ (Int :: *) => Int) -> Char -> Char
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType]
$cfoo_rCm = \ _ [Occ=Dead] (a2_aBf :: Char) -> a2_aBf

-- RHS size: {terms: 1, types: 0, coercions: 3}
Bug.$fFooChar [InlPrag=INLINE (sat-args=0)] :: Foo Char
[GblId[DFunId(nt)], Arity=2, Caf=NoCafRefs, Str=DmdType]
Bug.$fFooChar =
  $cfoo_rCm
  `cast` (Sym (Bug.N:Foo[0] <Char>_N)
          :: ((((Char :: *) ~ (Int :: *) => Int) -> Char -> Char) :: *)
             ~R#
             (Foo Char :: Constraint))

I'm not sure if I'm reading that correctly, but I think that instead of defining $cfoo_rCm in terms of $dmfoo, GHC is inlining the definition of $dmfoo directly into $cfoo (which has so far accounted for the difference between a succesfully typechecked program and one that fails).

comment:13 Changed 3 years ago by RyanGlScott

Cc: ekmett added

Sorry, my previous estimate was off the mark. It's not that the definition of $dmfoo is being inlined. Rather, after reading d2958bd08a049b61941f078e51809c7e63bc3354 more closely, the real culprit is that prior to that commit, default methods weren't being typechecked for each instance! As a result, the code was sneaking past the typechecker.

But I'm still confused as to why defining:

instance Foo Char where
  foo _ x = x

typechecks without issue (on all versions of GHC), but defining the instance in terms of a helper method:

fooDefault :: (a ~ Int => Int) -> a -> a
fooDefault _ a2 = a2

instance Foo Char where
  foo = fooDefault @Char

is rejected with an error.

cc'ing Edward Kmett on this one, since if lens really is using code that shouldn't typecheck, lens is going to need to come up with a workaround.

comment:14 Changed 3 years ago by goldfire

Oh gosh -- I've clearly been very confused. The original example makes sense to me only with a generic-default signature, so I assumed there was one. I've been thus babbling nonsense. Sorry, all!

I have no idea why including the method implementation works. I don't think it should.

But I still say the original code should be rejected for the same reasons I've already articulated. If inaccessible code were to become a warning, then the way to fix the warning is not to write the instance.

comment:15 Changed 3 years ago by RyanGlScott

Milestone: 8.2.18.0.2

Moving to 8.0.2, since this could cause lens to break if this change makes it in. Please revert if you disagree.

comment:16 Changed 3 years ago by ekmett

So am I correct in guessing that this causes us to fail for the Conjoined class in lens?

I've stripped it down removing the superclasses here:

class Conjoined p where
  conjoined :: ((p ~ (->)) => q (a -> b) r) -> q (p a b) r -> q (p a b) r
  conjoined _ r = r

(This is just a noisier version of Foo.)

This is a rather big huge of the optimization story in lens, as we use it to avoid fiddling around with updating indices when the user isn't using them. This can make a 100x difference in performance for user code, so it isn't a trivial thing to throw away. If this suddenly isn't legal any more I'm really not sure what the heck we're going to do.

That said, I don't see how that statement is illegal. conjoined takes two argument, one says _if_ you can tell me that p is (->) i'll give you a thing. The other is unconditionally usable.

Once you learn p isn't (->) you simply can't use the first argument, as you could never satisfy its precondition. It isn't an error on the behalf of the signature of conjoined. It seems something is hinky in the way we're judging who has incurred an obligation here and when.

We seem to be being far too eager to discharge an obligation we have no reason to even look at. Until something tries to use the first argument, why are we even doing anything with its constraints at all? The constraint being unsatisfiable in this limited situation is very much the point of the expression in the first place.

comment:17 in reply to:  16 Changed 3 years ago by mpickering

Ryan, I am very confused here. If I try the code from the ticket description, I can't call foo @Char so the defined instance is useless. Is this intentional? The same happens on GHC 8.0.1 and GHC 7.10.3.

*Foo> :t foo @Char
foo @Char :: (Char ~ Int => Int) -> Char -> Char
*Foo> :t foo @Char 5 'a'

<interactive>:1:1: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Inaccessible code in
        a type expected by the context:
          Char ~ Int => Int
    • In the second argument of ‘foo’, namely ‘5’
      In the expression: foo @Char 5 'a'

comment:18 in reply to:  16 Changed 3 years ago by mpickering

Replying to ekmett:

So am I correct in guessing that this causes us to fail for the Conjoined class in lens?

Yes this is where the example was reduced from.;

This is a rather big huge of the optimization story in lens, as we use it to avoid fiddling around with updating indices when the user isn't using them. This can make a 100x difference in performance for user code, so it isn't a trivial thing to throw away. If this suddenly isn't legal any more I'm really not sure what the heck we're going to do.

It seems that removing the constraint would preserve existing performance gains? Is the constraint used for something more than ensuring that only p ~ (->) can use the first argument and all other instances must use the default method?

comment:19 Changed 3 years ago by goldfire

Urgh. It seems I was even more confused than I realized in comment:14. Quite likely every word I've posted (hopefully not including these) is simply utter nonsense. Deep apologies. The confusion is entirely my own fault and not the result of anyone else's miscommunication. Let me try again.

Yes, this is a bug. We should indeed accept the original program without any warnings.

comment:20 Changed 3 years ago by ekmett

@mpickering:

Without the constraint none of the code that actually uses this combinator works at all. Those use sites exploit that extra bit of knowledge passed to the first argument by instance Conjoined (->) which knows p ~ (->) and therefore can use the first argument.

The typical workflow is to do something like

traversed :: Traversable f => IndexedTraversal Int (f a) (f b) a b
traversed = conjoined traverse (indexing traverse)

traverse requires its argument to be a function. indexing traverse isn't so picky and works for more choices of p.

Now using that if you use traversed as a simple Traversal it'll pick the fast traverse path, but if you need access to the numerical indices we put on each member, and use a combinator like itoListOf or (^@..), then it'll pay the price of computing indices in an extra bit of state. This is equivalent to traversing the original Traversable container with Compose (State Int) f and bumping the counter after visiting each member, rather than just using your original functor f. This is much much slower. traversed and indexing traverse should be indistinguishable for users, except for the fact that the former is much much faster for the common case.

comment:21 Changed 3 years ago by RyanGlScott

mpickering, I'm a bit confused too why foo 5 'a' itself doesn't typecheck, but that's not how lens is using this style of code. The way lens is using it, it's closer in style to something like this:

bar :: Foo a => a -> a
bar = foo 5

Now bar 'a' will typecheck.

Similarly, if you want a more complete lens-based piece of code to test against, you can use the following:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Lens where

indexing :: Indexable Int p => ((a -> Indexing f b) -> s -> Indexing f t) -> p a (f b) -> 
s -> f t
indexing l iafb s = snd $ runIndexing (l (\a -> Indexing (\i -> i `seq` (i + 1, indexed ia
fb i a))) s) 0

newtype Indexing f a = Indexing { runIndexing :: Int -> (Int, f a) }

instance Functor f => Functor (Indexing f) where
  fmap f (Indexing m) = Indexing $ \i -> case m i of
    (j, x) -> (j, fmap f x)

instance Applicative f => Applicative (Indexing f) where
  pure x = Indexing $ \i -> (i, pure x)
  Indexing mf <*> Indexing ma = Indexing $ \i -> case mf i of
    (j, ff) -> case ma j of
       ~(k, fa) -> (k, ff <*> fa)

type IndexedTraversal i s t a b = forall p f. (Indexable i p, Applicative f) => p a (f b) 
-> s -> f t

class Conjoined p where
  conjoined :: ((p ~ (->)) => q (a -> b) r) -> q (p a b) r -> q (p a b) r
  conjoined _ r = r

class Conjoined p => Indexable i p where
  indexed :: p a b -> i -> a -> b

---------------------------------------------------------------------

newtype Indexed i a b = Indexed { runIndexed :: i -> a -> b }

-- You'll need to comment out the instance below to typecheck on HEAD
instance Conjoined (Indexed i)

---------------------------------------------------------------------

-- This now typechecks:
traversed :: Traversable f => IndexedTraversal Int (f a) (f b) a b
traversed = conjoined traverse (indexing traverse)

The fact that foo 5 'a' doesn't typecheck might be part of the bug. As Edward mentioned above, I suspect that we are too eagerly discharging an obligation somewhere, and that explains:

  1. Why foo 5 'a' doesn't typecheck but bar 'a' does
  2. Why a manually implemented instance Foo Char where foo _ a = a typechecks but a default instance Foo Char doesn't

But these are just my suspicions.

comment:22 Changed 3 years ago by simonpj

Currently

foo :: (Char ~ Int => Int) -> a -> a
foo _ a2 = a2

gives a similar message. Is that reasonable? The argument to foo can't be called.

Instance decls are a bit different because you can change the type signature. Eg here is a simpler example

class C a where
  foo :: (a~Int) => a -> a

instance C Bool where
  foo = undefined

The instance decl is rejected, by both GHC 7.10 and HEAD. But of course there's nothing you can do about it. foo can't be called, but it needs something for the method foo. (It works when you leave out the definition of foo altogether, but I think only by accident.)

What we need is NOT to complain about inconsistent 'givens' when typechecking instance methods. And certainly not to fail.

Would that serve? It would sadly mean that inaccessible code somewhere deep in the body of an instance method wouldn't be reported, but maybe that's a lesser evil.

I have not followed all this stuff about Conjoined. Is it all the same question?

comment:23 Changed 3 years ago by ekmett

I think there is morally a difference between

class Foo a where
   foo :: (a ~ Int => a) -> a -> a

and your example which is more like

class Foo a where
   foo :: (a ~ Int) => a -> a -> a

in terms of if we should reject things once we know a ~ Char, and that hence a ~ Int can never happen.

In the former you're given two arguments, one of which requires you to provide something impossible to use, and so simply cant be used, while in the latter you're required to implement a contradiction when you go to write instance Foo Char.

Notice the polarity of the equality constraint. In the former it is in positive position. In the latter it is in negative position as usual. Finding a contradiction in negative position fits with Richard's intuition about if we should complain, but in positive position it simply means that argument is inaccessible, which is perfectly okay.

Someone might pass it in in a more polymorphic setting where they don't know if the constraint could be satisfied or not, until the instance for Foo is selected, which is what is happening here.

Today I usually hack around the latter by passing an explicit Dict for the constraint, so that I have the option to bring it into scope or not, and can carefully avoid GHC prematurely detonating upon discovering the contradiction

class Foo a where
   foo :: Dict (a ~ Int) -> a -> a -> a

but until now I haven't had to hack around it for the former -- and the explicit Dict-based solutions are much clunkier to both write, and for users to use in practice. (We used to use this approach to implement ex falso quodlibet in the constraints package, but now we just use Any directly as an uninhabitable initial Constraint.)

Currently

foo :: (Char ~ Int => Int) -> a -> a
foo _ a2 = a2

gives a similar message. Is that reasonable? The argument to foo can't be called.

I'd personally think that that should be allowed, as silly as it looks in this very concrete case. foo itself doesn't care about the argument at all. The burden of complaining about the impossibility of what we can see locally would be Int ~ Char should fall on type checking the argument passed to foo at the call site, not to foo, and at that call site it may or may not be impossible as it may not know the Int part of the equation there.

comment:24 Changed 3 years ago by ekmett

That said, I certainly wouldn't complain if both of those things started type checking.

comment:25 Changed 3 years ago by mpickering

I also apologise. Like Richard, I missed the fact that the constraint was appearing in the positive position. Sorry for all the confusion!

comment:26 Changed 3 years ago by simonpj

I agree with your reasoning, but it's quite painful to implement the positive/negative distinction (given the way the constraint solver works). Anything is possible, but this all seems a bit exotic, so I'm inclined to look for a simple solution.

I think it would be simple to:

  • Not complain about inaccessible code in instance methods

Would that do?

Currently GHC tries to do co/contra checking for subsumption checking. If we just used equality on the LHS of arrow, I think the negative/positive problem would disappear. Which is an intesting strike in favour of that approach. That would mean that this would fail:

f :: (Int -> Int) -> Int

g :: (forall a. a-> a) -> Int
g = f

On the other hand, with the same signatures

g x = f x

would succeed. The current co/contra subsumption is clever, but tricky... eg every foray into impredicative polymorphism gives up on it. Maybe we should give up on it now.

Simon

comment:27 Changed 3 years ago by bgamari

Milestone: 8.0.28.2.1

This appears to be an issue only on GHC HEAD.

Last edited 3 years ago by bgamari (previous) (diff)

comment:28 Changed 3 years ago by simonpj

Description: modified (diff)

comment:29 Changed 3 years ago by Iceland_jack

Possibly related, should this complain or is it up to the caller to use it with a Monoid A instance in scope

import Control.Monad.Writer

data A = A

a :: MonadWriter A m => m ()
a = tell A

comment:30 in reply to:  26 Changed 3 years ago by dfeuer

Replying to simonpj:

I agree with your reasoning, but it's quite painful to implement the positive/negative distinction (given the way the constraint solver works). Anything is possible, but this all seems a bit exotic, so I'm inclined to look for a simple solution.

I think it would be simple to:

  • Not complain about inaccessible code in instance methods

Would that do?

That doesn't seem likely to solve the problem in general, and leads to an odd inconsistency. Unfortunately, I don't know enough about type checking to understand the problem with the positive/negative approach. If you can't make that work, I would personally prefer dialing back the inaccessible code error to a warning and being stingier about emitting it. Having to manually defer GHC's checking using Dict and such always struck me as unnatural and potentially fragile. If I state ex falso, I'm usually doing it on purpose.

comment:31 Changed 3 years ago by simonpj

Hmm. Maybe just report when it arises from a GADT pattern match. That is the primary use-case:

data T a where
  T1 :: T Int
  T2 :: T a
  T3 :: T Bool

f :: T Int -> Bool
f T1 = ...
f T2 = ...
f T3 = ...  -- We want to report this case as inaccessible

I'll think on that.

comment:32 Changed 3 years ago by ekmett

@Iceland_jack: That should complain. The only way for it to become solvable is for the user to supply an orphan instance. We could never supply any errors for unsatisfied instances if that worked.

comment:33 Changed 3 years ago by adamgundry

I agree that we should make the inaccessible code error into a warning. I'm on the fence as to whether that warning should automatically be suppressed in instance methods, or whether users should simply have to disable it themselves. It would be very useful for it automatically to be suppressed when checking generated code. See also #11066, #8128, #8740.

comment:34 Changed 3 years ago by simonpj

I propose (comment:31) to report an error for a Given insoluble (e.g. Int ~ Bool) only if

  • there is an enclosing pattern match
  • that binds some equalities

Otherwise silently ignore Given insolubles. That will resolve all the complaints here, I think.

It's possible that we should warn; but it'd have to be not in -Wall because in some cases (like the instance one above) you can't "fix" the program to avoid the warning. So for now I'm inclined just to silently ignore.

OK? Patch in preparation.

Simon

comment:35 in reply to:  34 Changed 3 years ago by dfeuer

Replying to simonpj:

I propose (comment:31) to report an error for a Given insoluble (e.g. Int ~ Bool) only if

  • there is an enclosing pattern match
  • that binds some equalities

Otherwise silently ignore Given insolubles. That will resolve all the complaints here, I think.

It's possible that we should warn; but it'd have to be not in -Wall because in some cases (like the instance one above) you can't "fix" the program to avoid the warning. So for now I'm inclined just to silently ignore.

OK? Patch in preparation.

Simon

Can you give an example or two of code that will still produce an error?

comment:36 Changed 3 years ago by simonpj

Can you give an example or two of code that will still produce an error?

Yes indeed: see comment:31.

comment:37 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 03541cba/ghc:

Be less picky about reporing inaccessible code

Triggered by the discussion on Trac #12466, this patch
makes GHC less aggressive about reporting an error when
there are insoluble Givens.

Being so agressive was making some libraries fail to
compile, and is arguably wrong in at least some cases.
See the discussion on the ticket.

Several test now pass when they failed before; see
the files-modified list for this patch.

comment:38 Changed 3 years ago by simonpj

Plus this

commit 5eeabe250a1de456f70af07bd3f507a32cb8e10e
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Sep 12 22:21:15 2016 +0100

    Test wibbles for commit 03541cba
    
    I must have failed to validate properly, sorry.
    These testsuite wibbles belong with
    
      commit 03541cbae50f0d1cdf99120ab88698f29a278159
      Author: Simon Peyton Jones <simonpj@microsoft.com>
      Date:   Fri Sep 9 17:42:42 2016 +0100
    
          Be less picky about reporing inaccessible code

 testsuite/tests/typecheck/should_fail/FDsFromGivens.hs     | 5 ++++-
 testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr | 4 ++++
 testsuite/tests/typecheck/should_fail/T10715.hs            | 4 +++-
 testsuite/tests/typecheck/should_fail/T10715.stderr        | 4 ++++
 testsuite/tests/typecheck/should_fail/T8392a.hs            | 2 ++
 testsuite/tests/typecheck/should_fail/T8392a.stderr        | 4 ++++
 6 files changed, 21 insertions(+), 2 deletions(-)

This should, I hope, unglue the log-jam of #12220 and #12533.

Simon

comment:39 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T12466, T12466a

comment:40 Changed 3 years ago by bgamari

Milestone: 8.2.18.0.2
Note: See TracTickets for help on using tickets.