Opened 4 months ago
Closed 3 months 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 )
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 4 months ago by
Description: | modified (diff) |
---|
comment:2 follow-up: 3 Changed 4 months ago by
comment:3 Changed 4 months ago by
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 4 months ago by
Architecture: | x86_64 (amd64) → Unknown/Multiple |
---|---|
Component: | Compiler → Compiler (Type checker) |
Operating System: | MacOS X → Unknown/Multiple |
Priority: | normal → highest |
Summary: | Compiling a library problem with a local 8.5 build → GHC 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.
comment:5 Changed 4 months ago by
Cc: | goldfire added |
---|
This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.).
comment:6 Changed 4 months ago by
Description: | modified (diff) |
---|
comment:7 Changed 3 months ago by
Keywords: | TypeInType added |
---|---|
Summary: | GHC HEAD typechecker regression involving overlapping instances → GHC 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 3 months ago by
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:10 Changed 3 months ago by
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.
comment:12 Changed 3 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → indexed-types/should_compile/T15122 |
Richard, I think you might enjoy the fix here.
You may have found a bug but it's impossible to say without knowing what you are trying to compile.