Failure to resolve type parameter determined by type family
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Proxy
-- Defined to get the type forall x . 'D x
data D where
D :: a -> D
type family F t :: D
-- Will try to create values of this type through the type family
-- F, i.e. G (F t)
data G (d :: D) where
G :: G ('D x)
-- This is rejected because the type variable x in 'D x is ambiguous.
-- But is it really? If there's an instance of F t then x is determined.
introG :: Proxy t -> G (F t)
introG _ = G
-- introG is well-typed if we add an equality constraint.
-- Can GHC not figure this out without our help?
introG' :: forall t x . ( F t ~ 'D x ) => Proxy t -> G (F t)
introG' _ = G
Here's the type error:
• Couldn't match type ‘F t’ with ‘'D x0’
Expected type: G (F t)
Actual type: G ('D x0)
The type variable ‘x0’ is ambiguous
• In the expression: G
In an equation for ‘introG’: introG _ = G
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |