Skip to content

GitLab

GHC
GHC
Open
Opened by Koz Ross@kozross

QuantifiedConstraints cannot refer to KnownNat

Summary

If you attempt to write a quantified constraint involving KnownNat, GHC will inform you that Class KnownNat does not support user-specified instances. Given that no instances are being defined here (see 'Steps to reproduce' for an example), this is at least an unclear error message. It's also strange that it's not possible to express quantified constraints with KnownNat.

Steps to reproduce

Attempt to compile the following code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}

module Baz where

import Data.Kind (Type)
import GHC.TypeNats (KnownNat, Nat)

class (forall n. KnownNat n => KnownNat (f n)) => Foo (f :: Nat -> Nat) where
  type Bar n :: Nat

This will emit the error message described in the summary.

Expected behavior

Either to compile, or to give an error message more indicative of what the true problem is.

Environment

  • GHC version used: 8.10.1

Optional:

  • Operating System: GNU/Linux
  • System Architecture: x86_64