HEAD is stricter about instance overlap involving nonlinear unification
The following program is accepted on GHC 8.10.2:
{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleInstances, KindSignatures, MultiParamTypeClasses, ScopedTypeVariables, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
module Overlap where
import Data.Kind (Type)
class Sub (xs :: [Type]) (ys :: [Type]) where
subIndex :: Int
instance {-# OVERLAPPING #-} Sub xs xs where
subIndex = 0
instance (ys ~ (y ': ys'), Sub xs ys') => Sub xs ys where
subIndex = subIndex @xs @ys' + 1
subIndex1 :: forall (x :: Type) (xs :: [Type]). Int
subIndex1 = subIndex @xs @(x ': xs)
However, it is rejected on HEAD with the following error:
Overlap.hs:14:13: error:
• Overlapping instances for Sub xs (x : xs)
arising from a use of ‘subIndex’
Matching instances:
instance (ys ~ (y : ys'), Sub xs ys') => Sub xs ys
-- Defined at Overlap.hs:10:10
instance [overlapping] Sub xs xs -- Defined at Overlap.hs:8:30
(The choice depends on the instantiation of ‘x, xs’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: subIndex @xs @(x : xs)
In an equation for ‘subIndex1’: subIndex1 = subIndex @xs @(x : xs)
|
14 | subIndex1 = subIndex @xs @(x ': xs)
| ^^^^^^^^
I believe the program should be accepted. Clearly Sub xs (x ': xs)
does not match Sub xs xs
! But for some reason GHC HEAD does not eliminate it from the candidate set. (This seems to be a fairly recent regression.)
Note: the unusual phrasing of the inductive Sub
instance is necessary for this program to be valid, but it does not actually seem necessary to trigger the bug. If the instance were to be written more simply as
instance Sub xs ys => Sub xs (y ': ys) where
then GHC 8.10 would reject the program at a later stage of instance resolution, claiming that [W] Sub xs xs
matches both instance declarations. This is because the instance head of the base case is no longer a substitution of the inductive case, which is necessary to consider an instance “more specific,” as noted in the overlapping instances section of the User’s Guide.
Notably, using the simplified declaration on HEAD still results in the program being rejected at an earlier step of the search process, complaining about the ambiguity of [W] Sub xs (x ': xs)
instead of [W] Sub xs xs
. This is unsurprising given the behavior seen above.