8.10: Overlapping instances claimed where there are none (or crash in 8.8)
Summary
The following snippet (some of the code coming from generics-sop
),
either sends GHC into endless allocation loop (8.8),
or produces a self-contradictory error message:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
import Data.Kind (Constraint)
import Data.Proxy (Proxy)
import Data.Typeable (Typeable)
-- First, `generics-sop` code, intact.
--
type family
AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
AllF _c '[] = ()
AllF c (x ': xs) = (c x, All c xs)
class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k])
instance All c '[]
instance (c x, All c xs) => All c (x ': xs) where
class Top x
instance Top x
type SListI = All Top
-- Next, user code, minimised.
--
data GADT
= forall (xs :: [*]) (a :: *)
. (Top a, All Typeable xs)
=> GADT
withSomePipe'
:: GADT
-> (forall (xs :: [*])
. (Proxy xs -> GADT)
-> GADT)
-> GADT
withSomePipe' GADT f = f (const GADT)
8.10.1 says there are overlapping instances, but only lists one,
which isn't terribly surprising, as there is indeed just one instance for Top
:
[nix-shell:~/lift]$ ghc ~/ghc-instance-self-overlapping[ghc-instance-self-overlapping.hs](/uploads/adca7101458489bc35d16ceaf00af943/ghc-instance-self-overlapping.hs).hs
[1 of 1] Compiling Main ( /home/desktop/repro.hs, /home/desktop/repro.o )
/home/desktop/repro.hs:1:1: error:
The IO action `main' is not defined in module `Main'
|
1 | {-# LANGUAGE AllowAmbiguousTypes #-}
| ^
/home/desktop/repro.hs:45:33: error:
* Overlapping instances for Top a0 arising from a use of `GADT'
Matching givens (or their superclasses):
Top a
bound by a pattern with constructor:
GADT :: forall (xs :: [*]) a. (Top a, All Typeable xs) => GADT,
in an equation for withSomePipe'
at /home/desktop/repro.hs:45:15-18
Matching instances:
instance forall k (x :: k). Top x
-- Defined at /home/desktop/repro.hs:30:10
(The choice depends on the instantiation of `a0')
* In the first argument of `const', namely `GADT'
In the first argument of `f', namely `(const GADT)'
In the expression: f (const GADT)
|
45 | withSomePipe' GADT f = f (const GADT)
Steps to reproduce
With either ghc 8.10.1 or ghc 8.8.3:
ghc repro.hs
Expected behavior
The compiler shouldn't contradict itself in the error message, and it certainly needn't crash, although the latter part was fixed in the new release.
Environment
- GHC version used: 8.8.3 / 8.10.1
Optional:
- Operating System:
- System Architecture: