Confusing error message: could not deduce from identical context
I am experimenting with compile time computation via type-level programming. I wanted to try a more complicated function, namely foldr
. The idea is to supply the first two arguments on the type level such that they are known statically at compile time. My reasoning is that this allows me to ensure that the resulting function of type [a] -> b
will be specialized and optimized for the cons
and nil
functions. I got to this code:
{-# LANGUAGE PolyKinds, ScopedTypeVariables, DataKinds, TemplateHaskell, TypeApplications, FlexibleContexts, AllowAmbiguousTypes, TypeOperators #-}
module Main where
import Prelude.Singletons
import Data.Proxy
import Data.Reflection
foldr' :: forall a b (cons :: a ~> b ~> b) (nil :: b). Reifies (FoldrSym2 cons nil) ([a] -> b) => [a] -> b
foldr' = reflect (Proxy @(FoldrSym2 @_ @_ @[] cons nil))
For this code GHC gives the error:
app/Main.hs:16:10: error:
• Could not deduce (Reifies (FoldrSym2 cons nil) ([a] -> b))
arising from a use of ‘reflect’
(maybe you haven't applied a function to enough arguments?)
from the context: Reifies (FoldrSym2 cons nil) ([a] -> b)
bound by the type signature for:
foldr' :: forall {t :: * -> *} a b (cons :: a ~> (b ~> b))
(nil :: b).
Reifies (FoldrSym2 cons nil) ([a] -> b) =>
[a] -> b
at app/Main.hs:15:1-106
• In the expression:
reflect (Proxy @(FoldrSym2 @_ @_ @[] cons nil))
In an equation for ‘foldr'’:
foldr' = reflect (Proxy @(FoldrSym2 @_ @_ @[] cons nil))
|
16 | foldr' = reflect (Proxy @(FoldrSym2 @_ @_ @[] cons nil))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This confuses me, for some reason GHC doesn't see that the context is equal to the required Reifies
constraint, or perhaps there is some hidden information that prevents GHC from resolving that constraint.
This is with GHC 8.10.4