Opened 20 months ago

Closed 20 months ago

Last modified 16 months ago

#14735 closed bug (fixed)

GHC Panic with QuantifiedConstraints

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.2.2
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T14735
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

From branch wip/T2893

{-# Language QuantifiedConstraints #-}
{-# Language StandaloneDeriving #-}
{-# Language DataKinds #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Language KindSignatures #-}
{-# Language FlexibleInstances #-}
{-# Language UndecidableInstances #-}
{-# Language MultiParamTypeClasses #-}
{-# Language RankNTypes #-}
{-# Language ConstraintKinds #-}

import Data.Kind

data D c where
  D :: c => D c

newtype a :- b = S (a => D b)

class C1 a b
class C2 a b
instance C1 a b => C2 a b

class    (forall xx. f xx) => Limit f
instance (forall xx. f xx) => Limit f

-- impl :: Limit (C1 a) :- Limit (C2 a)
-- impl = S D

infixr 5 :<
data Sig a = N a | a :< Sig a

data AST :: (Sig Type -> Type) -> (Sig Type -> Type) where
  Sym  :: dom a -> AST dom a
  (:$) :: AST dom (xx :< a) -> AST dom (N xx) -> AST dom a

deriving instance (forall xx. Show (dom xx)) => Show (AST dom a)

data Arith a where
  Plus :: Arith (Int :< Int :< N Int)

deriving instance Show (Arith a)

loading this program and evaluating Sym Plus works fine:

$ ghc-stage2 --interactive hs/175-bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( hs/175-bug.hs, interpreted )
Ok, one module loaded.
*Main> Sym Plus
Sym Plus
*Main> 

but we uncomment impl we get a panic!

GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( hs/175-bug.hs, interpreted )
Ok, one module loaded.
*Main> Sym Plus
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.5.20180128 for x86_64-unknown-linux):
	nameModule
  system df_a2VB
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
        pprPanic, called at compiler/basicTypes/Name.hs:241:3 in ghc:Name

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

*Main> 

Change History (12)

comment:1 Changed 20 months ago by RyanGlScott

Perhaps this is just me, but I think that it's pretty early to be submitting bug reports about -XQuantifiedContexts, since this is a feature that:

  1. Hasn't even landed in GHC itself (let alone been formally submitted for review)
  2. Is still subject to change

My suggestion would be to hold off until there's a Phabricator Diff for this, at which point you can dump all of your findings there :)

comment:2 Changed 20 months ago by simonpj

I like having the bug reports though, and it does no harm to have them as separate tickets, provided they are clearly signposted as being on a branch, which this one is.

comment:3 Changed 20 months ago by Iceland_jack

Keywords: wipT2893 added

I have no issue either way, if I do make new ones I will use the keyword wipT2893 so they're easier to track down

comment:4 Changed 20 months ago by RyanGlScott

Ah, OK. If Simon is alright with this state of affairs, then I have no objection :)

comment:5 Changed 20 months ago by simonpj

Keywords: QuantifiedConstraints added; QuantifiedContexts removed

comment:6 Changed 20 months ago by simonpj

Resolution: fixed
Status: newclosed

I think I've fixed this. Try again7

comment:7 Changed 20 months ago by simonpj

Commit is

commit e0d5286c8cea23ca27163abe76d63c1f10719fa2
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Jan 31 11:54:32 2018 +0000

    Move SCC on evidence binds to post-desguaring
    
    This fixes Trac #14735, and is generally nicer anyway.

comment:8 Changed 20 months ago by Iceland_jack

It works now, thanks

comment:9 Changed 17 months ago by Ben Gamari <ben@…>

In 7bb7f99/ghc:

Discard reflexive casts during Simplify

Trac #14735 (derived from Trac #11735) found that 75% of compile
time was being spent in simplCast. This patch is the first in a series
to deal with that problem.

This particular patch actually has very little effect on performance; it
just refactors simplCast so that it builds Refl coercions less often.
Refl coercions require us to compute the type to put inside them, and
even if that's done lazily it is still work and code. Instead we use
Maybe Coercion with Nothing for Refl. This change also percolates to
pushCoTyArg and pushValArg.

Reviewers: goldfire, bgamari, simonpj

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14737

Differential Revision: https://phabricator.haskell.org/D4395

comment:10 Changed 16 months ago by Ben Gamari <ben@…>

In 7df5896/ghc:

Implement QuantifiedConstraints

We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement.   All the machinery was
already in place.

The main ticket is Trac #2893, but also relevant are
  #5927
  #8516
  #9123 (especially!  higher kinded roles)
  #14070
  #14317

The wiki page is
  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.

Here is the relevant Note:

Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like
this:

  data Rose f x = Rose x (f (Rose f x))

  instance (Eq a, forall b. Eq b => Eq (f b))
        => Eq (Rose f a)  where
    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
 [W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.

Here are the moving parts
  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension

  * A new form of evidence, EvDFun, that is used to discharge
    such wanted constraints

  * checkValidType gets some changes to accept forall-constraints
    only in the right places.

  * Type.PredTree gets a new constructor ForAllPred, and
    and classifyPredType analyses a PredType to decompose
    the new forall-constraints

  * Define a type TcRnTypes.QCInst, which holds a given
    quantified constraint in the inert set

  * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
    which holds all the Given forall-constraints.  In effect,
    such Given constraints are like local instance decls.

  * When trying to solve a class constraint, via
    TcInteract.matchInstEnv, use the InstEnv from inert_insts
    so that we include the local Given forall-constraints
    in the lookup.  (See TcSMonad.getInstEnvs.)

  * topReactionsStage calls doTopReactOther for CIrredCan and
    CTyEqCan, so they can try to react with any given
    quantified constraints (TcInteract.matchLocalInst)

  * TcCanonical.canForAll deals with solving a
    forall-constraint.  See
       Note [Solving a Wanted forall-constraint]
       Note [Solving a Wanted forall-constraint]

  * We augment the kick-out code to kick out an inert
    forall constraint if it can be rewritten by a new
    type equality; see TcSMonad.kick_out_rewritable

Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Move SCC on evidence bindings to post-desugaring, which fixed
  #14735, and is generally nicer anyway because we can use
  existing CoreSyn free-var functions.  (Quantified constraints
  made the free-vars of an ev-term a bit more complicated.)

* In LookupInstResult, replace GenInst with OneInst and NotSure,
  using the latter for multiple matches and/or one or more
  unifiers

comment:11 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed

comment:12 Changed 16 months ago by RyanGlScott

Milestone: 8.6.1
Test Case: typecheck/should_compile/T14735
Note: See TracTickets for help on using tickets.