compiler ignores constraint on instance declaration
Steps to reproduce
Try to compile and run this program:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
import GHC.TypeLits
import Data.Proxy
class HasLength a where
type BitLength a :: Nat
bitLength :: forall a. (KnownNat (BitLength a)) => a -> Integer
bitLength _a = natVal (Proxy @(BitLength a))
data Test (n :: Nat) = Test
instance (n <= 10) => HasLength (Test n) where
type BitLength (Test n) = n
main :: IO ()
main = print $ bitLength (Test :: Test 20)
This program compiles and prints 20
when executed, which is not what I would expect.
Expected behavior
The program shall not compile, since there is no HasLength
instance in this case (n > 10
).
It behaves as expected when the function signature is changed to:
bitLength :: forall a. (HasLength a, KnownNat (BitLength a)) => a -> Integer
... that is, when explicit HasLength a
is added to the constraints. However, the compiler shall reject (or at least warn) the original version also, since it's clear that in order to have BitLength
, the HasLength
instance must also be defined.
Honestly, I am not sure if this is a bug or not. But it took me a while to find out that explicit HasLength
constraint is required in this case. It would be nice if GHC would give me some hint.
Environment
- GHC version used: 8.10.4
Optional:
- Operating System: ubuntu, nix package manager
- System Architecture: