GHC forgets constraints
Possibly related: #10338
The following program should compile, but fails with the error:
Could not deduce (Bar (F zq) zq) arising from a use of ‘bar’
from the context (Bar (Foo (F zq)) (Foo zq))
bound by the type signature for
bug :: Bar (Foo (F zq)) (Foo zq) => Foo (F zq) -> Foo zq
This is definitely incorrect: I am providing a Bar
constraint in the context of bug
, but GHC is asking for constraints so that it can resolve to the instance declared in Bar.hs.
A few workarounds I've found so far, which may or may not help find the bug:
- Adding
-XTypeFamilies
to Main.hs makes the program compile. -
Removing the type signature from
x
inbug
makes the program compile. - Defining
bug
without alet
asbug sk = bar sk :: Foo zq
orbug sk = bar sk
makes the program compile.
- *Main.hs:**
{-# LANGUAGE FlexibleContexts, ScopedTypeVariables #-}
module Main where
import Bar
bug :: forall zq .
(Bar (Foo (F zq)) (Foo zq))
=> Foo (F zq) -> Foo zq
bug sk =
let x = bar sk :: Foo zq
in x
- *Bar.hs**
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-}
module Bar where
type family F b
newtype Foo r = Foo r
type instance F (Foo r) = Foo (F r)
class Bar a b where
bar :: a -> b
instance (Bar a b) => Bar (Foo a) (Foo b)