Odd interation between ambiguity check, instance constraint, and fundeps
Summary
I suspect this might be related to #21149 (closed), but it doesn't look quite the same so I figured I'd report it anyway. A custom type error is reported in a situation where it's not at all obvious why the TypeError
in question is even being inspected.
Steps to reproduce
{-# language DataKinds, PolyKinds, FunctionalDependencies, AllowAmbiguousTypes, UndecidableInstances #-}
module AmbTE where
import GHC.TypeLits
import Data.Proxy
class xs ~ (hd ': tl) =>
HeadTail (msg :: ErrorMessage) (xs :: [k]) (hd :: k) (tl :: [k])
| xs -> hd tl, hd tl -> xs
instance xs ~ (hd ': tl) => HeadTail msg xs hd tl
instance {-# INCOHERENT #-}
(TypeError msg, '[] ~ (hd ': tl)) => HeadTail msg '[] hd tl
foo :: forall {k} (xs :: [k]) (hd :: k) (tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
foo = Proxy
This reports
AmbTE.hs:10:8: error:
• whoopsy
• In the ambiguity check for ‘foo’
In the type signature:
foo :: forall {k}
(xs :: [k])
(hd :: k)
(tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
|
10 | foo :: forall {k} (xs :: [k]) (hd :: k) (tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
Since I don't see any '[]
in that type signature, it seems rather surprising to get the type error!
After writing the above, I realized that the fundeps are actually redundant. Removing them, surprisingly, makes it compile!
Expected behavior
I'd expect the above to compile.
Environment
- GHC version used: 9.4.1
Optional:
- Operating System:
- System Architecture: