Strange constraint error that disappears when adding another top-level declaration
Consider this program:
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
module CURepro where
import Data.Kind
data NP (f :: Type -> Type) (xs :: [Type])
type family Curry (f :: Type -> Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where
Curry f xs r (f x -> a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
Curry f xs r a = (xs ~ '[], r ~ a)
type family Tail (a :: [Type]) :: [Type] where
Tail (_ : xs) = xs
uncurry_NP :: (Curry f xs r a) => (NP f xs -> r) -> a
uncurry_NP = undefined
fun_NP :: NP Id xs -> ()
fun_NP = undefined
newtype Id a = MkId a
-- test1 :: ()
-- test1 = uncurry_NP fun_NP (MkId 5)
test2 :: ()
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
With GHC 8.6.1 (and also 8.4.3), this produces the following error message:
CURepro.hs:27:9: error:
• Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’
arising from a use of ‘uncurry_NP’
The type variable ‘t0’ is ambiguous
• In the expression:
uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
In an equation for ‘test2’:
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
|
27 | test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
However, uncommenting the definition of test1
makes the whole program check without error!
I think both versions of the program should be accepted.
I've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that NP
is parameterised over a type constructor f
seems to be somehow essential to trigger this.
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |