Wednesday, February 24, 2021

[nzcimnev] infix dollar with RankNTypes

here is some surprising behavior seen with ghc 8.6.5 (Haskell compiler).

in the function "answer" at the end:

  1. infix dollar sign works
  2. using ($$) which is equal to ($) fails
  3. defining ($$$) exactly as ($) is defined in Prelude fails
  4. prefix dollar sign fails

in failures, always same two error messages, abbreviated here:

    * Couldn't match type `m' with `m0'
    * No instance for (KnownNat m0) arising from a use of `five'

i suspect infix $ is not a normal function; it seems to be getting special treatment by ghc.


{-# LANGUAGE RankNTypes #-}
-- next two needed for type signature of ($$$)
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Main where {
import qualified Numeric.Modular; -- https://hackage.haskell.org/package/modular
import GHC.TypeNats(KnownNat);
import GHC.Exts(TYPE);

main :: IO();
main = undefined;

five :: forall m . KnownNat m => Numeric.Modular.Mod m;
five = Numeric.Modular.mkMod 5;

mod3 :: (forall m . KnownNat m => Numeric.Modular.Mod m) -> Integer;
mod3 = Numeric.Modular.withMod 3;

($$) = ($);

-- copy the definition of ($) from Prelude
infixr 0 $$$;
($$$) :: forall r a (b :: TYPE r). (a -> b) -> a -> b;
f $$$ x = f x;
{-# INLINE ($$$) #-}; -- the semicolon is necessary!

-- compute 5 mod 3 = 2
answer :: Integer;
-- answer = mod3 five; -- works
answer = mod3 $ five; -- works
-- answer = mod3 $$ five; -- fails to compile
-- answer = mod3 $$$ five; -- fails to compile
-- answer = ($) mod3 five; -- fails to compile

} --end

No comments :