我试图打破Haskell并从GHC得到一个"无法访问的代码"错误.这是什么意思？

Question

所以,我有以下代码:

{-# LANGUAGE GADTs #-}

import Data.Coerce
import Data.Functor.Fixedpoint --Although I'm not using these yet, they provide "context"

data Refl a b where
    Refl :: Refl a a

weird :: Refl a [a] -> a
weird Refl = [[], [[], []]]

我想你可以看到我要去的地方.如果没有,我想要做的就是强迫Haskell思考a并且[a]通过赋予它Refl参数是相同的类型.这将允许我做恶作剧.当我编译它时,ghci给我这个错误:

[1 of 1] Compiling Main             ( pad'.hs, interpreted )

pad'.hs:9:7:
    Couldn't match type ‘a’ with ‘[a]’
      ‘a’ is a rigid type variable bound by
          the type signature for weird :: Refl a [a] -> [a] at pad'.hs:8:10
    Inaccessible code in
      a pattern with constructor
        Refl :: forall a. Refl a a,
      in an equation for ‘weird’
    Relevant bindings include
      weird :: Refl a [a] -> [a] (bound at pad'.hs:9:1)
    In the pattern: Refl
    In an equation for ‘weird’: weird Refl = [[], [[], []]]
Failed, modules loaded: none.

什么Inaccessible code意思？一般来说,有什么资源与我正在尝试做的事情相关吗？

Answer 1

它只是意味着无法weird使用非底部参数调用函数(即,使用终止,非异常提升表达式).

这是因为没有构造函数(或者更准确地说,没有WHNF)可以拥有Refl a [a]它的类型.实际上,类型a和[a]肯定是不同的,无论a可能是什么(并且这可以在统一期间检查).

由于这通常不是编程错误的来源,因此GHC错误地向程序员大声抱怨.

如果你真正想要做一个"不可能"的输入,请改用:

{-# LANGUAGE EmptyCase #-}
weird :: Refl a [a] -> a
weird x = case x of { }

甚至

{-# LANGUAGE EmptyCase #-}
weird :: Refl a [a] -> b
weird x = case x of { }

的确,weird实际上可以生产任何类型!无法呼叫,它可以为其输出声明任何类型.这遵循逻辑原则"ex falso quod libet":从错误的前提(例如,那个a和[a]相同的类型),你可以推断出你想要的任何东西.

最后说明,因为你导入Data.Functor.Fixedpoint,我想你想用Fix [].嗯,这是同构的[Fix []]- 但不相等!所以,再次,你不能有一个非底部的类型表达式Refl (Fix []) [Fix []].