Skip to content

Error with data instance and type operators #402

@ndmitchell

Description

@ndmitchell

From ndmitchell/hlint#450 by @LeanderK:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
module Test where

import           Data.Singletons.Prelude
import           Data.Singletons.TypeLits
import           Data.Type.Equality            ((:~:) (..), (:~~:) (..))

data instance Sing (z :: (a :~: b)) where
    SRefl :: Sing Refl

Gives a parse error on the :~:.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions