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: