Opened 7 weeks ago

Closed 4 weeks ago

#15122 closed bug (fixed)

GHC HEAD typechecker regression

Reported by: fmixing Owned by:
Priority: highest Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: indexed-types/should_compile/T15122
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by RyanGlScott)

This code, distilled from the type-level-sets library:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

data Proxy (p :: k) = Proxy

data Set (n :: [k]) where
    Empty :: Set '[]
    Ext :: e -> Set s -> Set (e ': s)

type family (m :: [k]) :\ (x :: k) :: [k] where
     '[]       :\ x = '[]
     (x ': xs) :\ x = xs
     (y ': xs) :\ x = y ': (xs :\ x)

class Remove s t where
  remove :: Set s -> Proxy t -> Set (s :\ t)

instance Remove '[] t where
  remove Empty Proxy = Empty

instance {-# OVERLAPS #-} Remove (x ': xs) x where
  remove (Ext _ xs) Proxy = xs

instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
      => Remove (y ': xs) x where
  remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)

Typechecks in GHC 8.4.2, but not in GHC HEAD:

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

Bug.hs:31:33: error:
    • Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x))
      from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
        bound by the instance declaration at Bug.hs:(29,31)-(30,27)
      or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*]))
        bound by a pattern with constructor:
                   Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s),
                 in an equation for ‘remove’
        at Bug.hs:31:11-18
      Expected type: Set ((y : xs) :\ x)
        Actual type: Set (e : (s :\ x))
    • In the expression: Ext y (remove xs x)
      In an equation for ‘remove’:
          remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
      In the instance declaration for ‘Remove (y : xs) x’
    • Relevant bindings include
        x :: Proxy x (bound at Bug.hs:31:22)
        xs :: Set s (bound at Bug.hs:31:17)
        y :: e (bound at Bug.hs:31:15)
        remove :: Set (y : xs) -> Proxy x -> Set ((y : xs) :\ x)
          (bound at Bug.hs:31:3)
   |
31 |   remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
   |                                 ^^^^^^^^^^^^^^^^^^^

This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.).

Change History (12)

comment:1 Changed 7 weeks ago by fmixing

Description: modified (diff)

comment:2 Changed 7 weeks ago by mpickering

You may have found a bug but it's impossible to say without knowing what you are trying to compile.

comment:3 in reply to:  2 Changed 7 weeks ago by fmixing

Replying to mpickering:

You may have found a bug but it's impossible to say without knowing what you are trying to compile.

type-level-sets library from https://github.com/dorchard/type-level-sets. It cannot be installed by cabal install because it is lacking of TypeInType extension in Data.Type.Set, so I downloaded it, added extension, imported import GHC.Types, * replaced with GHC.Types.*. So the current Data.Type.Set looks like https://gist.github.com/fmixing/695d46c6c5cc97398c3c44e05f23d764

comment:4 Changed 7 weeks ago by RyanGlScott

Architecture: x86_64 (amd64)Unknown/Multiple
Component: CompilerCompiler (Type checker)
Operating System: MacOS XUnknown/Multiple
Priority: normalhighest
Summary: Compiling a library problem with a local 8.5 buildGHC HEAD typechecker regression involving overlapping instances

Here is a slightly more minimal example:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

data Proxy (p :: k) = Proxy

data Set (n :: [k]) where
    Empty :: Set '[]
    Ext :: e -> Set s -> Set (e ': s)

type family (m :: [k]) :\ (x :: k) :: [k] where
     '[]       :\ x = '[]
     (x ': xs) :\ x = xs
     (y ': xs) :\ x = y ': (xs :\ x)

class Remove s t where
  remove :: Set s -> Proxy t -> Set (s :\ t)

instance Remove '[] t where
  remove Empty Proxy = Empty

instance {-# OVERLAPS #-} Remove (x ': xs) x where
  remove (Ext _ xs) Proxy = xs

instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
      => Remove (y ': xs) x where
  remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)

In GHC 8.4.2, this typechecks, but in GHC HEAD, it fails with:

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

Bug.hs:31:33: error:
    • Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x))
      from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
        bound by the instance declaration at Bug.hs:(29,31)-(30,27)
      or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*]))
        bound by a pattern with constructor:
                   Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s),
                 in an equation for ‘remove’
        at Bug.hs:31:11-18
      Expected type: Set ((y : xs) :\ x)
        Actual type: Set (e : (s :\ x))
    • In the expression: Ext y (remove xs x)
      In an equation for ‘remove’:
          remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
      In the instance declaration for ‘Remove (y : xs) x’
    • Relevant bindings include
        x :: Proxy x (bound at Bug.hs:31:22)
        xs :: Set s (bound at Bug.hs:31:17)
        y :: e (bound at Bug.hs:31:15)
        remove :: Set (y : xs) -> Proxy x -> Set ((y : xs) :\ x)
          (bound at Bug.hs:31:3)
   |
31 |   remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
   |                                 ^^^^^^^^^^^^^^^^^^^

I'm unclear on what the exact culprit is here, so feel free to change the title further if overlapping instances turn out not to be the problem.

Edit: I've changed the description to use this example.

Last edited 7 weeks ago by RyanGlScott (previous) (diff)

comment:5 Changed 7 weeks ago by RyanGlScott

Cc: goldfire added

This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.).

comment:6 Changed 7 weeks ago by RyanGlScott

Description: modified (diff)

comment:7 Changed 6 weeks ago by RyanGlScott

Keywords: TypeInType added
Summary: GHC HEAD typechecker regression involving overlapping instancesGHC HEAD typechecker regression

Never mind, I don't think this has anything to do with overlapping instances (or even type classes in particular), since the following also typechecks on GHC 8.4 but not on HEAD:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Proxy

data Set (n :: [k]) where
    Empty :: Set '[]
    Ext :: e -> Set s -> Set (e ': s)

type family (m :: [k]) :\ (x :: k) :: [k] where
     '[]       :\ x = '[]
     (x ': xs) :\ x = xs
     (y ': xs) :\ x = y ': (xs :\ x)

remove :: forall x y xs.
          ((y : xs) :\ x) ~ (y : (xs :\ x))
       => Set (y ': xs) -> Proxy x -> Set ((y ': xs) :\ x)
remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs))

remove' :: Set s -> Proxy x -> Proxy xs -> Set (xs :\ x)
remove' = undefined

Here's the error message on HEAD if you compile with -fprint-explicit-kinds:

$ /opt/ghc/head/bin/ghc -fprint-explicit-kinds Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:24:23: error:
    • Could not deduce: ((:\) * ((':) * e s) x :: [*])
                        ~~ ((':) * e ((:\) * s x) :: [*])
      from the context: (:\) k ((':) k y xs) x ~ (':) k y ((:\) k xs x)
        bound by the type signature for:
                   remove :: forall k (x :: k) (y :: k) (xs :: [k]).
                             ((:\) k ((':) k y xs) x ~ (':) k y ((:\) k xs x)) =>
                             Set k ((':) k y xs) -> Proxy k x -> Set k ((:\) k ((':) k y xs) x)
        at Bug.hs:(21,1)-(23,58)
      or from: ((k :: *) ~~ (* :: *),
                ((':) k y xs :: [k]) ~~ ((':) * e s :: [*]))
        bound by a pattern with constructor:
                   Ext :: forall e (s :: [*]). e -> Set * s -> Set * ((':) * e s),
                 in an equation for ‘remove’
        at Bug.hs:24:9-16
      Expected type: Set k ((:\) k ((':) k y xs) x)
        Actual type: Set * ((':) * e ((:\) * s x))
    • In the expression: Ext y (remove' xs x (Proxy :: Proxy xs))
      In an equation for ‘remove’:
          remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs))
    • Relevant bindings include
        x :: Proxy k x (bound at Bug.hs:24:19)
        xs :: Set * s (bound at Bug.hs:24:15)
        y :: e (bound at Bug.hs:24:13)
        remove :: Set k ((':) k y xs)
                  -> Proxy k x -> Set k ((:\) k ((':) k y xs) x)
          (bound at Bug.hs:24:1)
   |
24 | remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs))
   |                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

comment:8 Changed 6 weeks ago by RyanGlScott

OK, even smaller now:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Data.Proxy

data IsStar (a :: k) where
  IsStar :: IsStar (a :: *)

type family F (a :: k) :: k

foo :: (F a ~ F b) => IsStar a -> Proxy b
                   -> Proxy (F a) -> Proxy (F b)
foo IsStar _ p = p

comment:9 Changed 6 weeks ago by goldfire

I see this and will take a stab when I can.

comment:10 Changed 6 weeks ago by simonpj

I took a look. Not yet complete but may help Richard.

Analysing the program in cmmment:8.

foo :: (F a ~ F b) => IsStar a -> Proxy b
                   -> Proxy (F a) -> Proxy (F b)
foo IsStar _ p = p

Informally we have

 (a::k), (b::k)
 [G] F a ~ F b
 [G] k ~ *
 [W] F a ~ F b

The given k ~ * should rewrite both the given and wanted equality, which should allow us to prove it no problem.

The firsts slightly surprising thing is that the data constructor IsStar binds an existential:

IsStar : forall k (a::k). forall (a2::*). (k~*, a~a2) => IsStar @k a

Is this rigth? Well, if IsStar had some arguments it mmight be more persuasive

data IsStar2 (a :: k) where
  IsStar2 :: a2 -> IsStar a2

Now

IsStar : forall k (a::k). forall (a2::*). (k~*, a~a2) => a2 -> IsStar @k a

We can't have a on the LHS of the arrow, because it has the wrong kind.

Here's the implication we can't solve

 Implic {
   TcLevel = 2
   Skolems = k_a1hM[sk:2]
             (a_a1hN[sk:2] :: k_a1hM[sk:2])
             (b_a1hO[sk:2] :: k_a1hM[sk:2])
   No-eqs = False
   Status = Unsolved
   Given =
     $d~_a1hQ :: (F a_a1hN[sk:2] :: k_a1hM[sk:2])
                 ~ (F b_a1hO[sk:2] :: k_a1hM[sk:2])
   Wanted =
     WC {wc_impl =
           Implic {
             TcLevel = 3
             Skolems = a_a1hR[ssk:3]
             No-eqs = False
             Status = Unsolved
             Given =
               co_a1hS :: (k_a1hM[sk:2] :: *)            ~# (* :: *)
               co_a1hT :: (a_a1hN[sk:2] :: k_a1hM[sk:2]) ~# (a_a1hR[ssk:3] :: *)
             Wanted =
               WC {wc_simple =
                     [WD] hole{co_a1ig} {3}:: (F (b_a1hO[sk:2] |> co_a1hS) :: *)
                                              ~# (F a_a1hR[ssk:3] :: *) (CNonCanonical)}
             Binds = EvBindsVar<a1hV>
             a pattern with constructor: IsStar :: forall a. IsStar a,
             in an equation for `foo_a1hP' }}

Not yet sure why we can't solve it.

At the crucial moment in typechecking foo we see this:

  work item = [WD] hole{co_a1hU} {0}:: (F a_a1hN[sk:2] :: k_a1hM[sk:2])
                                       ~# (F b_a1hO[sk:2] :: k_a1hM[sk:2]) (CNonCanonical)
  inerts = {Equalities: [G] co_a1hS {0}:: (k_a1hM[sk:2] :: *)
                                          ~# (* :: *) (CTyEqCan)
                        [G] co_a1i4 {1}:: (fsk_a1i0[fsk:0] :: k_a1hM[sk:2])
                                          ~# (fsk_a1i2[fsk:0] :: k_a1hM[sk:2]) (CTyEqCan)
                        [G] co_a1i9 {1}:: (a_a1hN[sk:2] :: k_a1hM[sk:2])
                                          ~# ((a_a1hR[ssk:3] |> Sym co_a1hS) :: k_a1hM[sk:2]) (CTyEqCan)
            Type-function equalities = [G] co_a1ib {0}:: (F (b_a1hO[sk:2] |> co_a1hS) :: *)
                                                         ~# (fsk_a1ia[fsk:0] :: *) (CFunEqCan)
                                       [G] co_a1id {0}:: (F a_a1hR[ssk:3] :: *)
                                                         ~# (fsk_a1ic[fsk:0] :: *) (CFunEqCan)
            Dictionaries = [G] $d~~_a1i8 {0}:: ((fsk_a1i2[fsk:0] |> co_a1hS) :: *)
                                               ~~ ((fsk_a1i2[fsk:0] |> co_a1hS) :: *) (CDictCan)
                           [G] $d~_a1i7 {0}:: ((fsk_a1i2[fsk:0] |> co_a1hS) :: *)
                                              ~ ((fsk_a1i2[fsk:0] |> co_a1hS) :: *) (CDictCan)

Note these two lines:

  [G] co_a1hS {0}:: (k_a1hM[sk:2] :: *)               ~# (* :: *) (CTyEqCan)
  [G] co_a1i4 {1}:: (fsk_a1i0[fsk:0] :: k_a1hM[sk:2]) ~# (fsk_a1i2[fsk:0] :: k_a1hM[sk:2]) (CTyEqCan)

The first can rewrite the second, but we have not made it do so. I think because the substitution does not claim to be idempotent.

But then we end up trying to prove that

[W] fsk1 :: *  ~  fsk2 : *

and we have somehow lost the connection to our 'givens'. That's as far as I got.

Last edited 5 weeks ago by simonpj (previous) (diff)

comment:11 Changed 4 weeks ago by Simon Peyton Jones <simonpj@…>

In a32c8f75/ghc:

Use dischargeFunEq consistently

Trac #15122 turned out to be interesting.

* Were calling dischargeFmv in three places.

* In all three cases we dealt with the Given case
  separately.

* In two of the three cases the Given code was right,
  (albeit duplicated).

* In the third case (in TcCanonical.canCFunEqCan), we had
     ; case flav of
         Given -> return () -- nothing more to do.
  which was utterly wrong.

The solution is easy: move the Given-case handling into
dischargeFmv (now reenamed dischargeFunEq), and delete it
from the call sites.

Result: less code, easier to understand (dischargeFunEq handles
all three cases, not just two out of three), and Trac #15122 is fixed.

comment:12 Changed 4 weeks ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T15122

Richard, I think you might enjoy the fix here.

Note: See TracTickets for help on using tickets.