GHC error message quotes type family definition verbatim-CodePudding

The code below results in an error message that, at first glance, appears to imply that GHC doesn't understand the definition of the type family WrapParams :

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits( Nat, type (-) )
import Data.Kind( Type )

newtype Wrapped a = Wrapped a

-- |
-- E.g., `WrapParams 2 (Int -> String -> Bool)` is `Wrapped Int -> Wrapped String -> Bool`
--
type family WrapParams (n :: Nat) (f :: Type) where
  WrapParams 0 f = f
  WrapParams n (p -> f) = Wrapped p -> WrapParams (n - 1) f


-- |
-- E.g., `extendToWrappedParams @2 ( ) (Wrapped 1) (wrapped 2)` is supposed to be 3.
--
class ExtendToWrappedParams (n :: Nat) (f :: Type)  where
  extendToWrappedParams :: f -> WrapParams n f

instance ExtendToWrappedParams 0 t where
  extendToWrappedParams t = t

instance (ExtendToWrappedParams (n - 1) f) => ExtendToWrappedParams n (p -> f) where
  extendToWrappedParams g = h
    where
      h (Wrapped p) = extendToWrappedParams @(n - 1) @f (g p)

Here's the error (using GHC 8.10.7):

• Couldn't match expected type ‘WrapParams n (p -> f)’
              with actual type ‘Wrapped p -> WrapParams (n - 1) f’
• In the expression: h
  In an equation for ‘extendToWrappedParams’:
      extendToWrappedParams g
        = h
        where
            h (Wrapped p) = extendToWrappedParams @(n - 1) @f (g p)
  In the instance declaration for ‘ExtendToWrappedParams n (p -> f)’

The first two lines quote the definition of WrapParams verbatim, giving the impression that GHC somehow didn't understand it. Obviously, that can't be what's actually happening - so, what am I missing? Is there any way (apart from resorting to unsafeCoerce) to make the code above compile?

CodePudding user response：

WrapParams n (p -> f) equals Wrapped p -> WrapParams (n - 1) f only when n is not 0. There is no direct way to express unequality in Haskell. Usual workarounds include switching to Peano naturals, or branching off boolean comparisons (Data.Type.Equality.==) instead of pattern-matching on Nat so you can write (n == 0) ~ 'False as a constraint.