Cannot deduce constraint from itself with poly-kinded type family
Compiling
{-# LANGUAGE PolyKinds, TypeFamilies #-}
module Eq where
type family F a :: k where
withEq :: F Int ~ F Bool => a
withEq = undefined
gives an arguably confusing error message:
Eq.hs:7:11: error:
• Could not deduce: F Int ~ F Bool
from the context: F Int ~ F Bool
bound by the type signature for:
withEq :: forall k a. (F Int ~ F Bool) => a
at Eq.hs:7:11-29
NB: ‘F’ is a non-injective type family
The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘withEq’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: withEq :: F Int ~ F Bool => a
I'm not claiming this program should necessarily typecheck, but "Cannot deduce X from the context X" induces head-scratching.
Replacing k
with *
in the definition of F
makes the error go away.
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |