Skip to content

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:
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information