haskellghctype-families

GHC error message quotes type family definition verbatim


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?


Solution

  • 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.